Comment by Veserv
2 hours ago
You have a serious misunderstanding of the consequences of the undecidability of the Halting Problem. The Halting Problem says you can not prove the precise halting behavior in every problem. Precise and every are very important qualifiers.
If you sacrifice precise and widen it to: "Halt" and "Maybe run forever, but might just take longer than the age of the universe and is thus irrelevant for actual programs we might choose to run" then it is decidable for every problem.
Every means that there exist programs, in the infinity of all programs, that can not be proven. It does not mean that no program can be proven. Programs that are 10^8000000 instructions long that are intentionally obfuscated count in every. Human-designed programs that humans want to be correct and are reasonably sure are correct are extremely well-behaved in comparison and their provable termination can almost always be reasoned about.
Generally speaking, human-designed programs are almost always implicitly being constructed in the space of programs that will terminate (possibly relative to a event loop). At every step of the process you only extend using provably terminating constructions. Few humans will have a loop condition like: "Terminates if the Goldbach Conjecture is true" which is one of those sorts of things that makes it hard to prove termination. Just stay away from unproven conjectures in your loop conditions and you will probably be fine.
No comments yet
Contribute on Hacker News ↗