In a Turing complete language, the halting problem prevents you from proving formally that any program has certain properties (say, that it doesn't leak memory).
In a language where any program halts by construction, the compiler can actually check such properties.
In a language where any program halts by construction, the compiler can actually check such properties.