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