News for hackers. Stuff that matters.

A comment on Lean – Theorem Prover. Parent comment

Re:Lean – Theorem Prover by nextos on Friday January 20, 2023 @10:43PM (#34463658)
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

[2] https://news.ycombinator.com/item?id=22794533

[ Parent | on HN ]
Re:Lean – Theorem Prover by kevinbuzzard on Saturday January 21, 2023 @01:49PM (#34469019)
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 is a book more suited for programmers, although it is in Lean 3 and right now the community is migrating to Lean 4.
[ Parent | on HN ]