[crote]

But you can do some static analysis on it. There is most likely a very common set of patterns known to terminate, a rare-but-expected set of patterns known to never terminate, and an infinite set of rare patterns which is unknown.

Rust is doing basically the same thing. Default code is "safe", and the compiler is able to prove its correctness. If the compiler can't make heads or tails of it, you have to put it in "unsafe" - and the programmer is expected to check the correctness herself.