> Isn't it the case that you can only prove that a program halts if it can be reduced/transformed to a computational model (e.g., a model that is effectively ca

> Isn't it the case that you can only prove that a program halts if it can be reduced/transformed to a computational model (e.g., a model that is effectively calculable) that is less powerful than a Turing machine? Models less power than a turing machine are still incredibly powerful. Some useful general purpose languages only accept programs that terminate. Hell, every useful program I ever wrote could be (in principle) proved to halt (excepting a `while True: do useful terminating thing again` main loop, of course).