For the program to be guaranteed to finish in theory, all that is required is that a valid proof exists. You don't have to pick a length in advance - the program just has to keep trying proofs of progressively longer lengths.
For the program to be guaranteed to finish in theory, all that is required is that a valid proof exists. You don't have to pick a length in advance - the program just has to keep trying proofs of progressively longer lengths.
But it won't finish if there is no proof! A halting oracle will finish either way.
Sure, but neither bcrypt or chess fall into the category of being unprovable, so having a halting detector doesn't help for those situations. The author is mixing up problems that are "hard" in the sense that we know in principle how to solve it but need a lot of resources, versus "hard" in the sense that we genuinely don't know how to solve the problem, even if we had access to infinite resources.
Mixing these two up is very misleading and detracts from what is otherwise a well written article.
This is a fair point, and I conceded it above in one of my first replies.