3 ms·

No, that's a misunderstanding. It says you can't come up with a general algorithm for arbitrary programs to detect whether they will halt, it says nothing about

• hajile 4y ago
  That is true in theory, but not in practice. A large program is itself essentially composed of many subprograms. You must prove every single aspect of those subprograms (hard in and of itself) then you must prove that every possible combination of those subprograms is also provable. As there is no general formula for the halting problem, each combination must be uniquely proven. This essentially means that if you have N possible branches, then the difficulty proving for each unique case would be the factorial of N. Proving 9kloc of code for L4 took 5-10 man years. Adding just 1kloc of similarly dense code would likely add decades of man-years. What about 100kloc or 1mloc? Even if you could find tricks to optimize similar branches, the fundamental factorial problem doesn't go away (as making it go away would mean that you've solved the provably insolvable halting problem). In practice, only the most trivial of programs are completely provable before the heat death of the universe.