[tsimionescu]

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.