> Turning program correctness into just a matter of type safety, at which point it is just compositional.

It isn't. "Truth-preservation" in all deduction systems is also compositional (if the premises are true, so is the conclusion); that doesn't make the propositions compositional with respect to program components (if I conclude that X > 3 and Y > 2, then I can also conclude that X + Y > 5; the conclusion preserves the truth of the premises, not the property itself, as neither X nor Y is greater than 5). If you have a property of a program that isn't a property of a component, then the property is not compositional (note that type safety is: A∘B is type-safe iff A and B are; but type safety here is merely the inference step, similar to truth preservation). If it's not compositional, it can be arbitrarily hard to prove.

> Maybe there are important cases that we can't solve this way, but I've not encountered any yet.

If you're able to affordably prove any correctness property of any real-world program, this knowledge is worth billions. I am not aware of anyone who's ever made a similar claim.

> I'd argue that we already do huge amounts of program verification with deductive proofs - that is, typechecking - many orders of magnitude more code is typechecked than has any other formal method applied - and the frontier of progress is how much we can represent important program properties within that.

But the properties proven are easy. It's like saying, I can jump 50cm, so jumping all the way to the moon is just a matter of degree. No. There are real, fundamental, theoretical barriers between proving compositional properties and non-compositional ones (or those that require one or two inferences and ones that are more); between proving properties with zero or one quantifier, and properties with two quantifiers.

Also, while you can be pleased with Haskell's formal accomplishments, have you compared them to those of model checking in safety-critical real-time systems? Because once you do, you realize it doesn't look so good in comparison.

And your comparison of Haskell and Java is particularly interesting. You say that Haskell's type systems is "streets ahead". I agree (although I think this comes at a great cost). However, Haskell correctness or development cost is not "streets ahead" or even noticeably ahead. This shows that strengthening some deductive property is no guarantee to improving quality. Why? Because software correctness is very complicated. Its theory is complicated, and its practice is even more complicated.

> I don't see that using types forces anything any more than any other approach to specification

I think depdedent types are just redundant. You can get all or most of what give you without the inflexibility and the bad default using other means.

But look, I'm personally not too fond of dependent types in particular and deductive proofs in general, and consider them something you use when all else fails, and you have the money to spare. Others can be as bearish on model checking or concolic testing, paths that I think are more promising and I believe are seeing a bigger research investments. But what is certain is that no one has any idea whether we will find a way to drastically increase software correctness in the next twenty years, let alone which method will get us there. The one thing you can be sure of anyone who tells you they do is that they are simply unfamiliar with the different avenues explored or with many of the challenges involved (including social challenges).