Dependent types are an active area of research. They are one of several different avenues of research into program verification.

The problem is that both their proponents and detractors (as well as those of other verification approaches) confuse research and practice. Think of the field as early stages of pharmaceutical research; experiments in the lab show some promise as well as obstacles, but it's too early to tell which of the approaches, if any, would be able to work at a large scale in field conditions. As long as we don't confuse research and practice we can follow, enjoy and evaluate research on its own terms, rather than judging it based on criteria that may not be relevant at this stage. This is not to say that we cannot point out risks to field adoption, but research is research.

I, too, have my doubts about dependent types, but it's unfair to judge them harshly at this stage, when nobody knows how best to use them.