I wasn't claiming that it is not possible to analyze a program to detect known exploits. Rather that it is extremely probable that another exploit will be found

I wasn't claiming that it is not possible to analyze a program to detect known exploits. Rather that it is extremely probable that another exploit will be found after the last one has been patched, and it is impossible to prove otherwise. The halting problem doesn't prevent playing whack-a-mole against previous exploits, but it ensures that proving more exploits do not exist is impossible. That's why I think a turing-complete language for smart contracts is a poor choice.