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.