Your explanation is good, but your pseudocode doesn't match what you're saying about it. There is a bug. One way to write it would be:
def P (program, input):
if [program on input] halts:
true
else:
false
def Q (input):
if P(Q, input):
Q(input) # P says we halt, so we won't
else:
true # P says we don't halt, so we will
Now, calling P(Q, Q) is what shows the truth of the Halting Problem.
It may be hard to think of conceptually, but when you explicitly state it all, it's pretty easy. P is a program. Q can be a program with P embedded in it. This is not anything unrealistic at all. Furthermore, calling P on (Q, Q) is not all that strange either, until you consider the resulting behavior:
P(Q, Q) -> should return true if Q halts on Q and false otherwise
Q halts on Q:
P -> true
Q loops. P was wrong
Q doesn't halt on Q:
P -> false
Q exits. P was wrong again
As long as programs like Q are allowed in your language, P cannot exist. Now, if you constrain Q such that every loop and recursion includes a proof of completion* , you can write a program P.
* This is generally possible by annotating the loop with a mathematical proof that the looping mechanism is approaching a terminating condition)
It may be hard to think of conceptually, but when you explicitly state it all, it's pretty easy. P is a program. Q can be a program with P embedded in it. This is not anything unrealistic at all. Furthermore, calling P on (Q, Q) is not all that strange either, until you consider the resulting behavior:
As long as programs like Q are allowed in your language, P cannot exist. Now, if you constrain Q such that every loop and recursion includes a proof of completion* , you can write a program P.* This is generally possible by annotating the loop with a mathematical proof that the looping mechanism is approaching a terminating condition)