[jroesch]

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]

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

[kevinbuzzard]

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.