[Hirrolot]

Yeah, the main problem with dependent types being used in low-level programming is that they're now able to perform arbitrary computation. That's why I think castrated dependent types might do the trick, since if you accept only integer indices as parameters to types, then you can boil down type checking to constraint solving without actually performing arbitrary computation.

[zozbot234]

Strictly speaking, dependent types cannot really perform arbitrary computation (as usually implemented) because general recursion is restricted. And most real-world programs, especially systems programs, need general recursion. So, for all the supposed generality of dependent types, you end up with two quite separate feature sets for compile-time and run-time execution that can only share a comparatively trivial common subset.

[Hirrolot]

You can have general recursion with dependent types though. Theorem provers prohibit it because otherwise it'd render the system logically inconsistent, which is far less severe in programming than in mathematics. But I agree that a great deal of expressivity of dependent types would be lost if they're applied to systems programming, which is somewhat unfortunate.