3 ms·
I think this really depends on how much you're willing to assume. You are right of course that the general problem is intractable, because you'd end up having t
by tathougies 7y ago
I think this really depends on how much you're willing to assume. You are right of course that the general problem is intractable, because you'd end up having to analyze frameworks, system calls, kernels, etc. But if you are able to assume those function as stated, then yes, you can certainly prove limited facts. For example, the sel4 microkernel is proven correct. Part of this proof of correctness is that all system calls do terminate.
But, actually, the most straightforward way to show that most 'everyday' programs terminate is -- assuming functionality of the language runtime as stated -- that they typically consist of non-recursive functions or functions on structurally smaller inputs. It would be obnoxious, but not difficult to show that a program like 'grep' terminates, assuming functionality of the operating system and hardware on which its running. This is actually fairly straightforwards, and many many functional languages with a focus on correctness have totality checking builtin. For example, Idris and Agda.
Of course, if you're going to ask to prove both functionality of the operating system (like Linux + glibc) or the processor itself, then that could indeed be trickier. But, if you limit your stack, it's certainly possible. The truth is that most computing does not consist of solving Turing complete problems.
- xyzzyz 7y agoSure, with some copious assumptions about the environment, you can prove without great difficulty that many real world programs do terminate. But it has really nothing to do with the Halting Problem, and saying that "halting problem is easily solved in practice" is extremely misleading.
- tathougies 7y agoI mean in practice the halting problem is not a useful result either so... The halting problem is theoretically solvable on every computer known to mankind becayse every computer thus far is a finite state machine, not a turing machine. The halting problem on finite state machines is solvable (exhaustively check there are no loops -- the structural recursion check I suggested above is simply an optimization of this more general technique). Now if we are actually discussing in good faith, the halting problem is often used as a reason why a particular program analysis wont work. While a good guideline, it does not mean that there are particular classes of programs for which these analyses would work. If you can show this and show that these programs cover a good amount of useful programs, then you can construct analyses that a purely theoretical and cursory understanding of the halting problem would suggest you cant. Indeed several useful languages do just this