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
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).
(And yes, this is mostly orthogonal to why you would want dependent types - these are indeed not so useful when you have general proof.)
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
For which reason sorry?
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.
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.