Dependent Haskell is not sound (type in type, i.e. a type level version of Russell's Paradox, and lack of totality checking). Its primary purpose is not theorem proving per se, but rather unifying the explosion of GHC extensions that currently are weak approximations of a full dependently typed system. More than anything it is precisely an exercise in whether dependent types are useful even if you aren't getting 100% watertight assurances with them.

Sure the article is a bit exuberant, but I think you're being a bit harsh here. Yes the field of formal verification, from my amateur practitioner's point of view, is a mishmash of techniques right now, with no single technique that has quite the right ergonomic vs power ratio that dominates over all others. But as far as I can tell there is in fact a significant amount research being done in dependent types. Many programming languages now have very limited dependent types. GADTs are one form that shows up in e.g. OCaml, Haskell, and Scala. Indeed Jane Street had a blog post about how GADTs were surprisingly useful for them (https://blog.janestreet.com/why-gadts-matter-for-performance...). Ongoing research projects occur for languages such as Agda and Coq.

Just like with formal specification systems like TLA+ and Alloy where you don't need to specify in exhaustive detail what you're after to see significant value, you don't have to prove comprehensive theorems to derive significant value from dependent types. An easy, lightweight win is to leave behind value specific tokens when performing some sort of runtime check rather than trying to prove the runtime check (e.g. keeping track that yes I ran the isPrime function on this number, rather than proving that a number is actually prime), which you can then use to subsume pre/postcondition contract systems, since you can attach markers of arbitrary checks being made that don't necessarily affect the value (e.g. keep track that I did check this user ID against a blacklist before trying to use it elsewhere).

The main problem with dependent types as far as I can tell is that only very recently have we had languages that try to write actual programs with full-spectrum dependent types appear. Idris is really the only example I can think of. Languages like Agda are first and foremost provers. I suspect the vast majority of Agda programs are never run after they've typechecked.

As a result we have little idea of what good practices with full-spectrum dependent types looks like. I have suspicions it looks fairly different from the hacks that current statically typed languages try to use to approximate it. For example I suspect some correct by construction approaches to ordinary statically typed FP languages quickly spiral into monstrosities with full-spectrum dependent types that can be nicely sidestepped again with evidence of runtime checks instead of full proofs.

Even with Idris, we don't have people using these systems in anger. We don't know how much to expose of function implementations, how much a totality checker matters, how best to avoid proof infection (where because a low-level component demands a proper proof and that proof is used at runtime, you must deliver a valid proof and can't use some sort of TrustMe escape hatch of a null value that has any type). There are ideas. Idris 2 introduces a type system that distinguishes between proofs that are never used at runtime and runtime values, allowing users to safely use the TrustMe escape hatch if necessary. But there isn't a large community working with them while trying to ship business products.

That for me is the greatest promise of dependent types in Haskell. Getting more real world experience of programmers using dependent types to uncover ergonomic holes. The Haskell community in the grand scheme of languages is small. It is nonetheless orders of magnitude larger than the full-spectrum dependently typed community and, if Dependent Haskell lands, represents perhaps the first time that a dependently typed language is used to directly write, rather than verify, production systems.