[colorint]

Yes, that was Turing's proof. Church's more indirect proof is that it's impossible to prove the equivalence of two lambda expressions. But the real essence of the problem is more like, you can't generally know ahead of time all the values that will be presented inside loop bodies. If you try to actually elaborate the loop then you get caught again: if the elaboration of the loop keeps going on for a while, the problem is re-presented, at what point do you give up? Which is to say, will this program, with these inputs, run forever? But this is basically Church's proof, since this is also the question, am I in exactly the same configuration as before? Without an ability to decide lambda expression equivalence, that question is also hopeless.

Hence the work that gets done in this area constrains the problem down to situations in which you can know enough to decide halting, like traversal of lists or trees that are known to be finite. I bring this up because, when it comes to AI, people want more than this.