This is my understanding as well, and underlies my assertions above. After all, if a compiler can tell you for certain that any given program written in a Turing-complete language will terminate, then you've literally just solved the halting problem. :P