Comment by pron

The problem is that dependent types (and the very idea of "correctness by construction") suffer from fundamental, serious limitations -- both in theory and in practice -- that the author does not seem to be aware of. He also does not seem to be aware of all the other approaches for software verification and correctness (sound static analysis, model checking, concolic testing) that have so far shown greater promise, and formal methods research focuses on them rather than on dependent types (the approach that scales least and suffers from the most limitations); in fact, last I spoke with a dependent type researchers, he told me that now they're trying to weaken the soundness of their type systems (sort of gradual-dependent-types) to try and fight the problems types suffer from. I'm not saying dependent types don't have some uses, or that they won't change enough so they could play a central role in software correctness, but thinking that they're the future of software correctness (in their current form) shows a complete lack of familiarity with this field.