3 ms·
Greatly simplifying, the most important result in comparability is “the halting problem”, which means we have no way of telling, for any program, if given some
by CJefferson 3y ago
Greatly simplifying, the most important result in comparability is “the halting problem”, which means we have no way of telling, for any program, if given some input it will halt or run forever.
After that, it’s not surprising there is some BB we can’t solve, and it’s interesting to investigate which we can, and can’t, solve.
- nine_k 3y agoNot "for any program", but "for an arbitrary program". We can trivially prove that a program that always goes to the next step, without branching, always terminates. With more effort we can prove termination of certain segments with conditional jumps, certain forms of recursion and loops, etc. This is not purely theoretic: e.g. EBPF programs in the Linux kernel are only admitted if the kernel can prove that they terminahe. What we can't do is to prove it in an arbitrary case, without putting limits on the program's structure.