[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.