logical_verification_2025

It's interesting Lean is taking off in software engineering. Prior to the advent of LLMs & agents, Lean had almost zero use in software and was mostly focused on mathematics, with Isabelle and Rocq leading the way here. In fact, I asked Kevin Buzzard and others in the Lean community, and they simply shrugged. The exception was [1], a Lean-based text heavily inspired by Concrete Semantics [2], a cornerstone of Isabelle literature. The latter is, in essence, Winskel's classic semantics book [3], a standard textbook in programming language theory, with all proofs mechanically checked. More broadly, I'm wondering whether dependent types are the right abstraction or too powerful and heavy for humans to review and make sure specifications are aligned with intent. I've been working on automation for this for more than a year, and I've found refi

Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications. For SWE, the most mature option is probably Isabelle. It's also a classical theorem prover, and it's perhaps easier to start with something that doesn't have dependent types. A cool thing is that the canonical Isabelle book [1] has been rewritten in Lean [2]. [1] http://concrete-semantics.org [2] https://github.com/lean-forward/logical_verification_2025

I have been eyeing “The Hitchhiker's Guide to Logical Verification” but haven’t yet found the time to work through it. The 2025 edition material is at https://github.com/lean-forward/logical_verification_2025?ta... An older version (2022-2023) with video lectures is at https://lean-forward.github.io/logical-verification/2022/ind...

> there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary. I think that, at least in software engineering, his point has not been disproven. Isabelle (classical) has a great track record in software verification. I don't see it as something inherently inferior to Rocq (dependently typed), which also has a great track record. Lean doesn't have a great focus (yet?) on software verification. And Agda is also not mainstream on large-scale industrial verification. One interesting thing would be to compare Concrete Semantics [1] (Isabelle) vs The Hitchhiker's Guide to Logical Verification [2] (an approximate rewrite in Lean). I am still starting with the second one, so I can't say much yet, but it might be too basic to draw any conclusions. Ultimately, refinement types embedded in general-pur