4 ms·

As someone who’s never messed with a theorem prover but would like to, would it make sense to start with Lean? How is it different from Coq? And is Coq worth le

by sakras 4y ago

As someone who’s never messed with a theorem prover but would like to, would it make sense to start with Lean? How is it different from Coq? And is Coq worth learning before Lean?

jroesch 4y ago
Did a PhD half focused on verification and also very biased being an early Lean developer. imo the Lean tooling and everything is much better I personally would never use Coq again especially after writing 200kloc+ of it over a few years. It has improved a lot but still I think Lean has many things going for it including a large focus on programming and using your Lean programs directly (versus extraction, which is roughly a really shitty compiler from Coq to Ocaml or another extracted language).
- nextos 4y ago
  However, the amount of teaching material focusing on software verification using Lean is frustratingly small? Coq has FRAP and CPDT [1], which teach you most techniques that are used in industry. Also Software Foundations. AFAIK, there's a version of Concrete Semantics using Lean [2]. But that's still just semantics. Any other materials focused on software verification, not on formalizing mathematics? [1] http://adam.chlipala.net http://adam.chlipala.net [2] https://news.ycombinator.com/item?id=22794533 https://news.ycombinator.com/item?id=22794533
  - kevinbuzzard 4y ago
    Yes. Coq has been around for decades and was adopted by the software verification community. Lean is much younger and its mathematics library caught on with the mathematician crowd, meaning that much of the Lean documentation right now is focused on mathematics. The hitchhiker's guide to logical verification https://cs.brown.edu/courses/cs1951x/static_files/main.pdf https://cs.brown.edu/courses/cs1951x/static_files/main.pdf is a book more suited for programmers, although it is in Lean 3 and right now the community is migrating to Lean 4.
deterministic 4y ago
I would recommend starting with Idris. It has all the power of a typical theorem prover but feels like a cool programming language. It also has a great book to bring you up to speed: “Type Driven Development”. It will blow your mind.

by sakras 4y ago

As someone who’s never messed with a theorem prover but would like to, would it make sense to start with Lean? How is it different from Coq? And is Coq worth learning before Lean?

jroesch 4y ago

Did a PhD half focused on verification and also very biased being an early Lean developer. imo the Lean tooling and everything is much better I personally would never use Coq again especially after writing 200kloc+ of it over a few years. It has improved a lot but still I think Lean has many things going for it including a large focus on programming and using your Lean programs directly (versus extraction, which is roughly a really shitty compiler from Coq to Ocaml or another extracted language).

nextos 4y ago
However, the amount of teaching material focusing on software verification using Lean is frustratingly small? Coq has FRAP and CPDT [1], which teach you most techniques that are used in industry. Also Software Foundations. AFAIK, there's a version of Concrete Semantics using Lean [2]. But that's still just semantics. Any other materials focused on software verification, not on formalizing mathematics? [1] http://adam.chlipala.net http://adam.chlipala.net [2] https://news.ycombinator.com/item?id=22794533 https://news.ycombinator.com/item?id=22794533
- kevinbuzzard 4y ago
  Yes. Coq has been around for decades and was adopted by the software verification community. Lean is much younger and its mathematics library caught on with the mathematician crowd, meaning that much of the Lean documentation right now is focused on mathematics. The hitchhiker's guide to logical verification https://cs.brown.edu/courses/cs1951x/static_files/main.pdf https://cs.brown.edu/courses/cs1951x/static_files/main.pdf is a book more suited for programmers, although it is in Lean 3 and right now the community is migrating to Lean 4.

deterministic 4y ago

I would recommend starting with Idris. It has all the power of a typical theorem prover but feels like a cool programming language. It also has a great book to bring you up to speed: “Type Driven Development”. It will blow your mind.