The halting problem is semi-decidable, which means that if a program terminates then it will always be able to be determined.
Some programs can be proven to terminate without running them, with say:
- typed theories, such as typed lambda calculus.
- Ackermann function
Are there some programs for which there is no other proof system except for the computation itself, where no properties of the program is know in advanced? And hence if so, it would make sense that some non-terminating programs, even though it can be proven to terminate eventually, we don't know how long that proof would take to compute, because it would not be known if the program simply needs to run for longer, because as stated above, not even the property of how long the program should run before we can determine if it should have terminated yet, is known in advanced.
Are there some programs for which the only proof of termination, is the actual running of the program, and waiting to see if it stops, no matter how long it takes to complete?