[lmm]

> Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly.

I'd say that's backwards: rather a dependently typed language relaxes a huge restriction that most programming languages have, that only certain things can be used as types. Any program that's valid in language X is also valid in a dependently typed version of language X (e.g. most Haskell functions translate directly into Idris as long as they don't rely on laziness).

Dependent types make it easier to encode properties that you care about into the type system, i.e. rather than the programmer having to get them right, the compiler can check them for you. Far from burdening the programmer, it lightens your mental load.

> All of the examples I've seen are about "index of a list is guaranteed in bounds". That is such a minor and infrequent bug in practice that it does not justify the additional complexity.

Most code is in terms of domain-specific things, and so the types you use are also domain-specific. In my experience every code bug (as distinct from "behaving as specified but not as intended" bugs) boils down to "we thought x, but actually y" and can be avoided by making more precise use of a type system. If you have bugs that hit production, you can probably avoid them with better types. If you avoid production bugs by using tests, you can probably replace most of those tests with types and they'll become more concise and easier to maintain. But of course the specifics of what types to use will be specific to your domain; examples like list indices are common because they're one of those rare types that virtually everyone uses.