alt Hacker NewsVery interesting. My takeaway is that Dr. Paulson's answer to the question is that there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary.
I would have liked to read more about Lean's alleged performance issues, and the issues around intentional equality. For the latter, I understand one can run into the need for heterogeneous equality (https://lean-lang.org/doc/reference/latest/Basic-Proposition...) when types are propositionally equal, but not definitionally equal. It has been some time I worked seriously in a dependently-typed language, but I recall coming to the conclusion that dependent types are best used as little as possible, for exactly this reason. If something may be stated as a theorem after the fact instead of putting it in the type, that was my preference.
Certainly there is something strongly aesthetically appealing about dependent type theory. The unification of programs and proofs and the natural emergence of independent proof objects. I am open to the idea that overly-dogmatic insistence on a type-theoretic basis to a theorem prover could lead to pragmatic issues, but I'd need to see more examples to be convinced there is a better foundation.
Anyway, I agree with Dr. Paulson's point that dependent types aren't necessary to verify interesting systems. He talked more of pure mathematics, but I am more interested in software verification. I work heavily in ACL2 which, not only does it not have dependent types, it doesn't have static typing at all! It is, however, also a first order logic and the both of these facts can sometimes be frustrating. Various libraries have been introduced to simulate typing and higher-ordered reasoning.
Replies
This is why dependent types work for modelling maths: you don't actually use your proofs as programs. Sure, the formalism would allow you to, but since you don't care about lemmas like "this proof and that proof are _the same_ for certain kinds of 'inputs,'" you don't run into issues with dependent types. If you try using dependent types, lemmas like the above quickly become necessary and also quickly become unprovable.
Talking about non-necessary is IMO a cop-out: I bet we can verify systems with even fewer features that he is using, or just a different set of features that get him to the same spot. The interesting question is always whether a feature is useful enough.
You get into types at the end. And sure, we don't need static types. Just like, outside of verification, we don't need garbage collection, or bounds checking, or even loops. But are the features useful? What takes us to the goal faster? And remember that also changes depending on who is doing the tasks. A lot of differents in tooling selection, across all kinds of work, come down to preference, not general utility, and they sure have nothing to do with necessity
>It has been some time I worked seriously in a dependently-typed language, but I recall coming to the conclusion that dependent types are best used as little as possible, for exactly this reason.
For which reason sorry?
> 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
[3] https://github.com/hwayne/lets-prove-leftpad