I'm currently teaching a class on computability and recently covered the proof that the halting problem is undecidable. I know of three major proof avenues that can be used here:
- Diagonalization - show that if the halting problem were decidable, we could build a machine that, if run on itself, is forced to do the opposite of what it says it will do.
- Recursion theorem - show that if the halting problem were decidable, then we could build a machine that obtains its own description, determines whether it halts on its input, then does the opposite.
- Reduction - show that some other undecidable problem reduces to the halting problem.
While I completely understand these proofs and think that they're mathematically beautiful, many of my students are having trouble with them because none of the proofs directly address why you can't tell if a program will halt. Nothing in the above proceeds along the line of "computations can evolve in a way that is so complicated that we can't predict what will happen when we start them up" or "machines can't introspective on themselves at that level of detail." I often give these intuitions to my students when they ask why the result holds, but I'm not aware of any formal proofs of that form.
Are there any proofs of the undecidability of the halting problem that directly explore why it's impossible for a program to decide what another program will do?
Thanks!