A tank is a way of getting people to work faster than walking, a concern that almost all people have, but that doesn't mean we should propose tanks for that purpose. That dependent types could increase correctness doesn't mean they should be added to a language -- unless its goal is research. This is a common problem I see. Say A is some business concern. The question we need to answer to decide whether to use solution B is not B => A but A => B.
What you're saying is that if I choose to use technique X and I want to achieve Y, then this is a way to do it. This is not the same as saying this is a good technique of achieving Y. The logical implication is reversed from what we'd like to find out. At best you're saying if you use dependent types, you increase correctness. I want to know what you should do to increase correctness, and using dependent types might be the worst possible option. The question is not whether dependent types imply increased correctness, but whether wanting increased correctness implies we should use dependent types. In fact, the post cites a case study about dependent Haskell that isn't exactly a glowing review of the feature.
> And these are good alternatives for some classes of problem, but how would I use them to type check a SQL query?
"Type-checking a SQL query" is not a business goal, and if I try to convert it to some goal you may have been referring to, for example, what is a good way to check if there are mistakes of some simple class in a SQL query, then I'm not sure simple testing isn't more than sufficient. Having said that, I like simple type systems, and I think they are also sufficient for that (e.g. there are typesafe SQL libraries for Java).
> Hmmm I have my doubts that this is really fit for such a purpose, otherwise why are there various efforts to build a deterministic JVM?
I don't know what the requirements are so I don't know.