Halting problem explanation and complete proof in 1 minute #VeritasiumContest

Can you explain and proof halting problem undecidability in 1 minute? - Yes!
I tried to explain it fast, but in a simple easy terms, that is why I decided to use pseudo-code. If you don't understand some part of the proof, ask me in the comments - I'll try to reply to all. To make the proof formal, you'll need to use (or define yourself) some specific language.

This proof is typically portrayed as merely a proof idea/concept, but after pondering about it for quite some time, I am convinced that this is a complete proof.

In short: it is correct because there are no errors

I expect though there will be disagreement regarding this, so I welcome discussion in the comments.

I have nothing against at what they've done and I actually find it pretty cool, but also quite funny.

Music "Everything Where it Needs to Be - Nat Keefe & Hot Buttered Rum" from YouTube Audio Library

[mind-blowingmath]

This proof is typically portrayed as merely a proof idea/concept, but after pondering about it for quite some time, I am convinced that this is a complete proof.
In short: it is correct because there are no errors
In long: it would not be complete in lambda-calculus computational model, but it is complete in "standard" computational model, by which I mean typical programming languages like JavaScript or Python, where functions can reference themselves and you have access to function content/definition/code by reference. Try running "(function f() { return f.toString(); })()" in JavaScript, for example.


I expect though there will be disagreement regarding this, so I welcome discussion in the comments.

[KarmaPeny]

As you have watched my video on this topic you will no doubt expect me to disagree with you, which I do. We can make the problem much simpler in order to properly consider what would happen to real world programs. Instead of trying to cater for all programs we could just consider ones that do one of these three things: 1) always halt, 2) always loop via calling a function that we might call 'start_looping', 3) ones that run the predictor program (which you have called 'halts') inside a sandbox & then do the opposite of whatever is predicted.

You might find that you go down an unending rabbit hole of nested calls and so you might think that this must be yet another kind of endless loop, but it doesn't have to do that. The predictor program might examine the input program and work out that it would be futile to try to do anything and so it might as well just give up. In both cases, it cannot beat the sneaky program that does the opposite. What I am saying here is that it is possible for the predictor program to identify what is going on. So it could do something about it if the environment allowed. It is only due to all the other restrictions that have been placed in its way that prevent the predictor from giving the right answer.

We could apply the same logic to the detection of a divide-by-zero operation for programs that we know halt at some point. So our sneaky program would run the predictor in a sandbox and do the opposite of what is predicted. Our sneaky program could detect if we were going down an endless loop of nested calls or if the predictor has crashed or otherwise failed to give answer, and then it could force-stop any looping and randomly choose between encountering divide-by-zero or not. Should we then conclude that it is impossible to predict if a program (that we know halts) will encounter a divide by zero problem?

Of course it isn't. The real world solution involves run-time routines, and possibly hardware or software interrupts. Then we could have an empty container as our predictor program that simply runs the program being tested (because we know it halts). If it fails due to a divide-by-zero then we could interpret this as 'the predictor says it will fail' and any other result we could take as a pass.

There is a problem with this approach because we haven't followed the halting problem spec to the letter. Our prediction program should really be a proper program that reports nicely rather than us just running the code to see what happens.

But this is just a niggling complaint because the fact remains that it is not impossible to predict if any given program that we know halts will encounter a divide-by-zero error or not. The very fact that we can achieve this by simply running the test program should tell us that the logic we used to come up with "it must be impossible" is not correct. If this is not concrete evidence of invalid logic in the halting problem proof then I don't know what is.

[geistar]

In our universe every program halts someday, one way or another. By itself or by the death of the universe.

[namihiko]

I don’t believe in the halting proof because it fundamentally does not prove the premise by contradiction. The premise is that the halting program indeed does determine if a program halts or doesn’t half GIVEN the input “W”. But all these “proofs” don’t work because they feed it input “W” and then feed it input “G” and are surprised that they get two different answers… hello?!!! You have it two different inputs and it gave you two different answers, it seems to be working just fine!

[syllabusgames]

You are making an awful lot of assumptions about your audience, and it's extremely detrimental to the value of the video. I'm a C# programmer and while I have written some python to make Blender addons, I have never encountered sum() before. While it is likely pretty intuitive, the aspect ratio of the video interfering with the code's spacing mixed with your complete lack of any explanation of the the code itself resulted in me not taking in any information I could explain to someone else. Building an input:output table of the first couple loops could have cleared this up a little.
For your Program f explanation, it would have been much more helpful if you graphed out both possible routes, showing the recursion and self-contradiction inherent to your example by showing the process for f returning both true and false. Also, the text messages don't really add anything.
I have only ever seen 1 good video on the halting problem. I think it was by Ben Eater, but evidently "halting problem" didn't make it in the title, so I can't find it. Sorry about that.