jacobt comments on A Series of Increasingly Perverse and Destructive Games

[jacobt]

For every n, a program exists that will solve the halting problem for programs up to length n, but the size of this program must grow with n. I don’t really see any practical way for a human to write this program other than generating an extremely large number and then testing all programs up to length n for halting within this bound, in which case you’ve already pretty much solved the original problem. If you use some proof system to try to prove that programs halt and then take the maximum running time of only those, then you might as well use a formalism like the calculus of constructions.

[loup-vaillant]

I don’t really see any practical way for a human to write this program other than generating an extremely large number and then testing all programs up to length n for halting within this bound, in which case you’ve already pretty much solved the original problem.

Wait, its even worse. A human in a room is an algorithm, and as such cannot solve the halting problem. There’s got to be some programs we just can’t know if they will halt or not. Which means there’s got to be an n beyond which some programs of length n or less cannot be analysed by humans.

That, or we have some special magic in us.