Yeah, type checking becomes undecidable otherwise and the compiler can also become vulnerable but Rust says they're going to try, so we'll see.

Well it's luckily a little better than that. Type checking doesn't have to be undecidable and the compiler doesn't have to be vulnerable because you don't have to execute any side effects in the compiler even if the code is meant to execute any side effects at runtime.

It's more that the utility of dependent types is generally restricted to functions that are pure and deal with immutable values, which means one possibility is to specially mark which of your functions are allowed to be used in a dependent type and which aren't. But the fragment of your program that can be used in dependent types is generally going to be a pure FP fragment.

Side effects aren't the only reason the compiler can be undecidable though. It depends on the type system, not just referential transparency. Look at Cayenne or ATS. Also, don't forget it's possible to still possible to DoS the system (although this is already more than possible with C++ and such, so what are we complaining about.)

Yeah, dependent types would be nonsensical for code that isn't functional. Marking which parts are and aren't is a good idea. Idris did something similar for totality checking. I think it'd be nice to have a system which differentiated between functions and procedures though.

> I think it'd be nice to have a system which differentiated between functions and procedures though.

That's essentially what 'IO' types are for (or finer-grained alternatives like 'Eff', etc.). At the value level, we have things like 'do notation', 'for/yield', etc.