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.<p>The exception was [1], a Lean-based text heavily inspired by <i>Concrete Semantics</i> [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.<p>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 refinement types sufficient and much easier to review.<p>[1] <a href="https://github.com/lean-forward/logical_verification_2025" rel="nofollow">https://github.com/lean-forward/logical_verification_2025</a><p>[2] <a href="http://concrete-semantics.org" rel="nofollow">http://concrete-semantics.org</a><p>[3] <a href="https://direct.mit.edu/books/monograph/4338/The-Formal-Semantics-of-Programming-LanguagesAn" rel="nofollow">https://direct.mit.edu/books/monograph/4338/The-Formal-Seman...</a>