[1]: Yes, I think this is possible. [2]
So I guess my point is: Does it really matter that you can come up with arbitrary programs that I will be unable to determine if they halt, if I can build up an entire OS platform of provably correct machine code with correctness proofs that I can scan out of a file to verify?
Ultimately, here's the point of re-framing it like this in the first place:
Now it's just a tooling problem.
I recognize that this is a very big 'just'.
The halting verifier program V never accesses itself. It takes two parameters: a program to check for halting (P) and an input to the program (I). It's job is to test whether P(I) (the program applied to the input) will halt.
To trick the halting verifier V we construct a diabolic P like this:
program P(I) {
if (V(I, I) == YES) { // if Verifier says I(I) halts
inifinite_loop(); // ... then do *not* halt
} else {
halt(); // ... otherwise halt
}
}
Given that P, we ask the verifier the devastating question: V(P, P).
Does P halt if given itself as input; does P(P) halt?
V cannot decide. Note that if we consider P(P), then it means that in the above program, the input parameter I becomes P itself: I = P. And so the V(I, I) == YES expression is actually testing V(P, P) == YES.
But V(P, P) is the devastating question itself!
If V(P, P) yields YES (P(P) halts) P goes into an infinite loop (P(P) in fact fails to halt), and so V has calculated the wrong answer: the actual behavior of P(P) contradicts the YES answer from V(P, P), rendering V incorrect. The same problem occurs if V(P, P) yields NO.
Note that P contains no self refererence. The fact that P is applied to itself as P(P) doesn't come from P; it comes from the way P is used. P is used that way when we ask the verifier V(P, P). The verifier itself is checking what happens if P is given itself as input. P can happily accept other programs as the input I, programs which are not itself.
What P needs is a way to embed V, because it relies on it. The assumption is that whatever halting verifier V someone tries to develop, it has to be public. So that is to say, some CS researcher claims he or she has developed a universal halting verifier algorithm V and they publish it. Then, promptly, their adversary takes the algorithm V and sticks it into their program P(I) as a subroutine, and has an instant test case which defeats V.
The tricky thing is not self-reference, but the fact that P contains the verifier and turns it against itself. The self-reference is instigated from the outside by choice of inputs. In other words, the devastating question V(P, P) is what perpetrates the self-reference which breaks V.
Now, all I have to do is write a program that includes an embedded version of your program. My program reads in the contents of itself and passes it to the embedded program. Now, all my program has to do is take the output of the embedded halt checker, and do the opposite; if the halt checker says the program halts, just keep looping. If it says I don't halt, exit immediately.
Now, you might think this is cheating, because it is using your own program against you. However, this is at the core of the problem; it has to work for ALL programs, even ones written with knowledge of your program.