[zozbot234]

> currently it's not quite clear what's the best way to integrate dependent types with systems programming.

Dependent types dispense with the phase separation between compile-time and run-time code, which is inherent to system languages. So you can easily have dependent types in a systems language as part of compile-time evaluation, but not really as a general feature. It would work quite similar to the "program extraction" feature in current dependent-language implementations, which does enable improved type checking because you can express arbitrary proofs and check them reliably as part of compilation.

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