alt Hacker News> 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-purpose languages might be a more pragmatic approach. Leftpad proofs using Rust Creusot, Dafny, or LiquidHaskell are quite straightforward [3], but again this is just a toy problem.
[1] http://concrete-semantics.org
[2] https://github.com/lean-forward/logical_verification_2025