Significant verification projects always plan for verification and do verification in tandem. That may be the case, but the point is that dependently type

Significant verification projects always plan for verification and do verification in tandem. That may be the case, but the point is that dependently typed programming languages force you to verify every intermediate step, while program logic gives you the option to do so. A key problem in contemporary software engineering is that specifications constantly change (aka "customers don't know what they want"). Agile software engineering methodologies have mostly taken over from waterfalls because agile is designed from the start to minimise the cost of change (how successful they are at minimise the cost of change is another matter). If you have to redo not just the code itself and tests but also proofs every time your customer changes the spec, the costs of software development increase rapidly. Look at e.g. Java exception specifications, for a similar but much more benign problem. The program logic approach to verification does not force the full cost of verification on the programmer, because verification can be deferred until the program specification is stable and it's code passes all tests. This enables a hybrid approach to program correctness: in early states of the software engineering process, you use lightweight methods such as Hindley-Milner like typing systems, and testing, and only in later states you go for logic-based approaches. Let me repeat that the program logic approach always allows you to specify and verify from day one, so program logic gives you the best of both worlds. Dafny and similar tools can only express first order logic That's a design choice of Dafny's and orthogonal to dependent types vs program logic. Moreover, all program logics where observational completeness has been proven(which means you can prove exactly the program properties that are contextually observable) were based on first-order logic. This is a pretty good indication that higher-order is not needed for sheer expressivity. Higher-order logics are but a convenience that enables shorter specifications and proofs. This is a silly point. First off proof assistants like Coq aren't inconsistent with the law of the excluded middle It's a serious point. Look at the influential nominal approaches to handling bound names. The reason they were implemented in Isabelle and are heavily used there, but are basically not used in Coq, despite nominal techniques being perfectly constructive, is that nominal techniques have extremely short and uniform non-constructive proofs which can easily be handled by Isabelle's proof automation, while the corresponding constructive proofs are long, non-uniform and not easily handled by Coq's proof automation. The real reason everybody uses dependent types is that they are perfectly matched for the verification of pure functional programs, since proofs are pure functional programs. This is beautiful. But as soon as you want to verify non functional programs, that beautiful coincidence evaporates. This is another key shortcoming of the dependent types approach: it's unlikely that it can be extended in a beautiful way to low-level programming, stateful programming, timed programming, concurrent programming.