Comment by program_whiz
4 hours ago
Wasn't the original proof something like "a program that loops indefinitely when the oracle says it will halt, and stops immediately if an oracle says it will not stop"? The whole point was the you can construct a contradictory program that cannot be decided by any oracle by its very nature.
```python
source_code = open(__file__, 'rt').read()
response = ask_llm("will this program halt, only answer 'yes' or 'no'?\n" + source_code)
will_halt = response == 'yes'
while will_halt:
continue```
You're right of course, LLMs provide a partial, unsound oracle.
The "halting problem is unsolvable" argument relies on the oracle not being able to output "not sure". But adding that option admits trivial oracles, like ones which output "not sure" for everything, so some are better than others.
The "real world" use most people have for halting oracles is as part of software safety, where if the checker outputs "not sure" you modify the software until the checker can decide if it halts.
Even if we had an answer to the halting problem, from a practical point of view, it's solving the wrong problem anyway. There's no point in distinguishing a function that would run forever from one that would exit after a century. They are both too slow.
Knowing that functions terminate is important for proof languages like Lean, where you often want to prove things without running the code at all. You're proving that one could, theoretically, calculate an answer, without actually calculating it.