<story><title>Functional Programming in Lean</title><url>https://leanprover.github.io/functional_programming_in_lean/</url></story><parent_chain><item><author>d_christiansen</author><text>Lean 4 is an interactive theorem prover. It&amp;#x27;s also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It&amp;#x27;s intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.</text></item></parent_chain><comment><author>ykonstant</author><text>Thank you very much for this book.  It has been invaluable for my introduction to Lean and a joy to study from.  I still have not read the last chapter, looking forward to it!  Kudos for your effort, and I hope you will write some more stuff about Lean in the future.</text></comment>
<story><title>Functional Programming in Lean</title><url>https://leanprover.github.io/functional_programming_in_lean/</url></story><parent_chain><item><author>d_christiansen</author><text>Lean 4 is an interactive theorem prover. It&amp;#x27;s also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It&amp;#x27;s intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.</text></item></parent_chain><comment><author>mdm12</author><text>Congratulations on the publication! As a dabbler in strictly typed functional programming languages like Scala and F#, I have always been curious about proof-oriented languages such as Coq or Agda, but found it difficult to justify the time investment. Lean seems to position itself as a theorem proving language that also supports general-purpose programs. Looking forward to digging into your book!</text></comment>