Very 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.

▲

nextos 4 days ago | parent | next [-]

> 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

▲

hibikir 4 days ago | parent | prev | next [-]

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

▲

Gajurgensen 4 days ago | parent [-]

I think the question of "necessity" is interesting, because between establishing that something is necessary vs the best option, I'd say the former is easier. And by agreeing that dependent types are not necessary (at least for certain design goals) we give space to the folks creating new provers to experiment with alternatives, which I think that is a good thing. I have been extremely impressed during my limited interactions with Lean, but I'm also vaguely aware of enough pain points to be interested in what other provers can do without being based on curry-howard.

Anyway, for what its worth, I generally agree that static typing is preferable. It is just a little more complicated in the context of theorem provers (as opposed to general-purpose, non-verification programming languages) where, for provers not based on type theory, propositions and proof obligations can be used where we might otherwise use types. This can be nice (generally more flexible, e.g. opportunities for non-tagged sums, easy "subtyping"), but also can be a downside (sometimes significant work reproducing what you get "for free" from a type system).

	▲	zozbot234 4 days ago \| parent [-]
		There are "provers not based on type theory", most notably the Mizar system, that still prefer types (where possible) to propositions and proof obligations. Mostly, because type checking and type inference are inherently a lot more efficient than fully-general proof checking and automated proving - hence it's convenient to have a separate formalism for the efficient subset of logic that's restricted to such "taxonomy-like" reasoning. (There is a similar case for using restricted "modalities" instead of fully-general first order logic for reasoning over "possible worlds": that too involves a significant gain in efficiency.) (And yes, this is mostly orthogonal to why you would want dependent types - these are indeed not so useful when you have general proof.)

▲

jojomodding 4 days ago | parent | prev | next [-]

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.

	▲	zozbot234 4 days ago \| parent [-]
		There are some theories like HoTT where it's convenient to let the same terms act as proofs while still having computational content and sometimes a distinct identity ("proof relevance"). For example a "proof" of isomorphism that might be used to transfer results and constructions across structures, where isomorphisms can be meaningfully distinct. Of course you do retain a significant subset of purely logical arguments where no computational content is ever involved and "identity" becomes irrelevant again.

▲

throwthrow0987 3 days ago | parent | prev [-]

>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?

▲

Gajurgensen 3 days ago | parent [-]

I was referring to issues that arise around the need for heterogeneous equality.

As an example, consider the dependent vector type `Vec n`, which is an array of length `n`. An `append` function would have type `{n m: Nat} -> Vec n -> Vec m -> Vec (n + m)`. That is, it takes an array of length `n`, and array of length `m`, and produces an array of length `n + m`.

Now imagine that you want to show that `append` is associative. That is, for all `x: Vec n`, `y: Vec m`, and `z: Vec o`, you have `append (append x y) z = append x (append y z)`. We can't prove this because we can't even state the theorem; it is not well-typed. The left-hand side has type `Vec ((n + m) + o)`, while the right-hand side has type `Vec (n + (m + o))`. Those two length values are of course propositionally equal, but they are not definitionally equal in type theories like Lean or Rocq's. That is, the equality is not immediately apparent to the type checker, and so requires a proof. But even with a proof, the statement is ill-typed (because equality is "intentional", not "extensional"). So you have to use a heterogeneous equality operator which allows you to compare two values whose types are propositionally but not definitionally equal. This equality is generally more difficult to work with.

Obviously this whole problem goes away if we use a non-dependent array type, as opposed to something length-indexed like this `Vec` type. So unless there is some reason to use the indexed type (e.g., perhaps the compiler can emit more efficient code), I would just use the non-indexed types and prove separately anything I want to know about the length.

	▲	throwthrow0987 3 days ago \| parent [-]
		Thanks, very clear explanation.