It’s been very difficult for me to devote any time to dependent type theory and it’s associated programming languages. It seems incredibly complicated for fairly little gain, since mis-specifying programs is so common.

I’m much more fond of the TLA+ style thinking of using simple untyped set theory and model-checking to verify computations.