3 ms·

Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming lan

Lean 4 is an interactive theorem prover. It'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'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.

mdm12 3y ago
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!
- epgui 3y ago
  Agda and Idris both also position themselves similarly.
  - siknad 3y ago
    Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.
    - epgui 3y ago
      You may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).
- d_christiansen 3y ago
  Thanks! I hope you find it valuable! Those other languages are also definitely worth learning. Happily, there's lots of cross-transfer of ideas and skills between them, so learning one will make the others easier. I got my start in dependent types with Software Foundations and Coq, and that was very helpful when learning Agda and Idris later. Similarly, skills from them transferred quite readily to Lean.
ykonstant 3y ago
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.
- d_christiansen 3y ago
  Thank you for reading it, and I hope that the final chapter is also enjoyable for you. Right now, I plan to take a break - this book occupied every Saturday for about a year, and some time off is in order. But Lean is tons of fun, and I'd like to get back into it once I'm recovered a bit.
deleted 3y ago
[deleted]
Reitet00 3y ago
This looks very nice! Is epub version planned?
- d_christiansen 3y ago
  Unfortunately not. I wanted to produce PDF and epub versions in parallel with the HTML version, but getting those to be of sufficient quality would have blown the time budget for the project. There's some old code in the Git history for dumping the source to Pandoc's dialect of Markdown, from which I was going to generate those, but the differences in Markdown dialects are enough that it was a fair bit of work. Dropping a print version and focusing on epub could very well be faster, as I suspect that an mdbook->epub pipeline is less challenging than creating a quality print-ready PDF. But no plans right now.
pjmlp 3y ago
Congratulations on releasing it. Looking forward to read it during Summer time.

mdm12 3y ago

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!

epgui 3y ago
Agda and Idris both also position themselves similarly.
- siknad 3y ago
  Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.
  - epgui 3y ago
    You may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).
d_christiansen 3y ago
Thanks! I hope you find it valuable! Those other languages are also definitely worth learning. Happily, there's lots of cross-transfer of ideas and skills between them, so learning one will make the others easier. I got my start in dependent types with Software Foundations and Coq, and that was very helpful when learning Agda and Idris later. Similarly, skills from them transferred quite readily to Lean.

ykonstant 3y ago

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.

d_christiansen 3y ago
Thank you for reading it, and I hope that the final chapter is also enjoyable for you. Right now, I plan to take a break - this book occupied every Saturday for about a year, and some time off is in order. But Lean is tons of fun, and I'd like to get back into it once I'm recovered a bit.

deleted 3y ago

[deleted]

Reitet00 3y ago

This looks very nice! Is epub version planned?

d_christiansen 3y ago
Unfortunately not. I wanted to produce PDF and epub versions in parallel with the HTML version, but getting those to be of sufficient quality would have blown the time budget for the project. There's some old code in the Git history for dumping the source to Pandoc's dialect of Markdown, from which I was going to generate those, but the differences in Markdown dialects are enough that it was a fair bit of work. Dropping a print version and focusing on epub could very well be faster, as I suspect that an mdbook->epub pipeline is less challenging than creating a quality print-ready PDF. But no plans right now.

pjmlp 3y ago

Congratulations on releasing it. Looking forward to read it during Summer time.