This is an introductory book to programming in Lean 4, a pure functional language that started as a theorem prover at Microsoft Research by Leonardo de Moura. It is a dependently typed language similar to Idris, with many features inspired by Haskell.

Though definitely not a language “ready for prime time”, Lean is remarkably user-friendly with its clean syntax, hygienic macros, package system (inspired by rust’s cargo) and VSCode and emacs plugins.

If you are interested in pure functional programming and a taste of proof assistants, check the book out.