_Functional Programming in Lean_ is now done and out the door!
It's a free online book that describes using the interactive theorem prover Lean 4 as a programming language, without assuming any background in functional programming. You don't need to already know Haskell, OCaml, Rust, Scala, or Racket to read this book.
You can read it at https://leanprover.github.io/functional_programming_in_lean/ .
Thank you to everyone who's carefully read prereleases - it's much, much better than it otherwise would have been. The Lean Zulip is a great place to hang out.
Also, thanks to MSR for supporting this project, and to Leonardo de Moura for initiating it. It's been a lot of fun!
@d_christiansen can we buy it somehow? 🙂
@jonn It's free! No purchase necessary!
On a more serious noted, we ended up cutting the PDF and epub versions for time reasons. In an earlier version, there was code that translated from the mdbook dialect of Markdown to the Pandoc dialect, which allowed nice looking PDFs via TeX as well as nice epubs. But all the subtle little incompatibilities added up, and there wasn't time to make it happen in a way that we felt good about.
I would like to have a nice bound version, though. I'm old fashioned that way.
If you're looking to have something you can read away from the computer, the whole thing is CC-BY, so you can make your own and share it with your friends! I did most of my proofreading with a browser-based print-to-PDF on my Remarkable, which was comfortable.
@d_christiansen yeah, I know these trick.
The question was meant purely as a question about supporting your work (in exchange for a typeset PDF :D).
Maybe community should typeset it for you? :)
@jonn Microsoft supported the work quite well already - the best support you can give is to read the book carefully and learn what you can from it. Thanks for wanting to, though!
The work of a typeset version isn't just something like a LaTeX export. To be a quality print book, I'd also have to make an index, figure out how to conditionally export page references instead of internal hyperlinks, etc. I think it's more a task for the author than a community one.
@d_christiansen got it! Yeah, I know how hard it is to typeset print media.
@jonn I'd like to see a multi-format authoring tool for books that should work well both online and in print and on ereaders. That would be a fun project!