[fusiongyro]

Dependent typing is really neat, but it introduces some new problems. Namely, the type checker becomes Turing complete. We have other examples of this level of complexity turning out to be manageable (C++ templates, for example, and the Hindley-Milner algorithm which turns out to be super-exponential in the worst case) but the power of dependent typing is begging to be used and abused to a greater degree.

I have some hope for Rust because their type invariants system (I forget what they're calling it) lets you glue some of this information to variables in a compelling way without necessarily having to solve all the theoretical and practical problems that come with full dependent typing.

We'll see, I guess.