[hibikir]

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]

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]

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