Comment by less_less
7 hours ago
I agree to some extent with your thesis. But also you don't have to encode all the properties of the program in dependent types everywhere. You can have the implementation contain either no proofs or fairly few (e.g., termination and no UB, which can often be automatically discharged), and then separately prove things about it. E.g.
def function_spec bleh blah := math_blargh
def function_impl bleh blah := code_blargh
theorem function_correct: forall bleh blah, function_impl bleh blah = function_spec bleh blah := by { long proof }
or whatever. That way the function's spec and implementation remain separate and readable. In my limited experience, Lean code usually works more this way rather than having the whole function and its spec in a giant dependently-typed object. For imperative code you can also use Hoare triples and vcgen, but that's currently only partly baked (i.e. proving things is a giant pain).
Maintenance is still a headache. If you change a small piece of your code, you would then need to change all the proofs that refer to it, and then if the specs also changed then you need to change all proofs that refer to those specs, etc.
In my view, a major selling point of dependent types when it comes to reasoning, is that by bundling logical properties with a runtime value, they require no separate effort to prove the propagation of the logical properties as the value is moved around. That is why I mentioned them in the context of opaque types. This is especially useful with generics: when a type parameter is instantiated with a dependent type, all its occurrences instantly benefit from the strong typing.
They can also be used to enforce just enough constraints on the inputs of a function to make it total, but this comes down to the tradeoff between either leaving an error path in the program and proving its unreachability later, or not having this error path but immediately requiring the proof. In any case, as you mention, further properties can be proved later without altering the dependent type.
I do not intend to come off as overly negative about dependent types. They have their uses, but they can also bring a maintenance nightmare.