> Why is this interesting? You pay an extremely heavy price in terms of language complexity.
As you say, there is no free lunch. Not having a useful type system introduces its own complexity. It depends on what abstractions you find most useful.
The present limitations of dependently typed languages will not be limitations tomorrow. Evolution in the field of proof engineering is providing new frameworks for making proofs more compositional and being able to extract programs from the proofs. It's not amazing and super useful today but it's a lot better than it was even five years ago and I suspect will continue to improve.
> After all, your specification is just as likely to be buggy as your implementation code
If you can't think of the right theorems or specifications I doubt you will write a correct program.
One is a lot easier to reason about than the other.
> Even type-checking can easily become undecidable when the ambient typing system is too expressive.
I'm not sure I follow. I understand how type inference can become undecidable but how does a sound type theory end up this way? The judgement and inference rules for CoC are rather small [0].
> There is no free lunch.
I don't disagree. I still enjoy programming in C. And I might even choose it for a project. And if it so happened that I had certain requirements like the system had to be real-time and could not deadlock then... I might be making a trade off to write my proofs and specifications in another language than my implementation.
We're not at a place yet where we can extract a full program from a specification and not in a place where we can write dependently-typed programs with deterministic run times either.
I would like to have my cake and eat it too but that's where we are.
> Not having a useful type system introduces its own complexity.
I agree, I am not promoting dynamically typed languages. My intuition about this is more that there is a sweet-spot between automation and expressivity that gives you the best software engineering experience in most practical programming tasks. Milner's let-polymorphism is closer to that sweet-spot than full-on dependent types a la Calculus-of-Constructions
> extract programs from the proofs.
In practise you don't have specifications in > 95% of programming tasks. What, for example, is the full specification of a climate simulation, or of TikTok? One could argue that the shipped product is the (first and only) specification. Every program I've ever been part of constructing started from an informal, intuitive, vague idea what the software should do. This includes safety-critical software. To quote from a famous paper [1]: "We have observed that the errors we find are divided roughly evenly between errors in the test data generators, errors in the specification, and errors in the program."
> If you can't think of the right theorems or specifications I doubt you will write a correct program.
I strongly disagree. I have written many programs that are, as far as I can see, correct, but I am not sure I fully know why. Here is an example: the Euclidean algorithm for computing the GCD. Why does it terminate? I worked out my informal understand why at some point, but that was a lot later than my implementation.
More importantly: in practise, you do not have a specification to start off with. The specification emerges during programming!
> how does a sound type theory end up this
I'm not sure what you are referring to. Type inference and type checking can be undecidable. For example System F, a la Curry.
> extract a full program from a specification
Let me quip: Proof are programs! In other words: if you want to be able to extract a full program from proofs, the specification / proof must already contain all the information the eventual program should have. So any bug that you can make in programming, you also must be able to make in proving. Different syntax and abstraction levels clearly corresponds to to different programmer error probabilities. But fundamentally you cannot get away from the fact that specifications can and often do contain bugs.
[1] K. Claessen, J. Hughes, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs.
As you say, there is no free lunch. Not having a useful type system introduces its own complexity. It depends on what abstractions you find most useful.
The present limitations of dependently typed languages will not be limitations tomorrow. Evolution in the field of proof engineering is providing new frameworks for making proofs more compositional and being able to extract programs from the proofs. It's not amazing and super useful today but it's a lot better than it was even five years ago and I suspect will continue to improve.
> After all, your specification is just as likely to be buggy as your implementation code
If you can't think of the right theorems or specifications I doubt you will write a correct program.
One is a lot easier to reason about than the other.
> Even type-checking can easily become undecidable when the ambient typing system is too expressive.
I'm not sure I follow. I understand how type inference can become undecidable but how does a sound type theory end up this way? The judgement and inference rules for CoC are rather small [0].
> There is no free lunch.
I don't disagree. I still enjoy programming in C. And I might even choose it for a project. And if it so happened that I had certain requirements like the system had to be real-time and could not deadlock then... I might be making a trade off to write my proofs and specifications in another language than my implementation.
We're not at a place yet where we can extract a full program from a specification and not in a place where we can write dependently-typed programs with deterministic run times either.
I would like to have my cake and eat it too but that's where we are.
[0] https://en.wikipedia.org/wiki/Calculus_of_constructions