Comment Re:Oh, not again. (Score 1) 401
As a practical matter, there's a widely used program that tries to solve the halting problem by formal means - the Microsoft Static Driver Verifier. Every signed driver for Windows 7 and later has been through that verifier, which attempts to formally prove that the driver will not infinitely loop, break the system memory model with a bad pointer, or incorrectly call a driver-level API. In other words, it is trying to prove that the driver won't screw up the rest of the OS kernel. This is a real proof of correctness system in widespread use.
The verifier reports Pass, Fail, or Inconclusive. Inconclusive is reported if the verifier runs out of time or memory space. That's usually an indication that the driver's logic is a mess. If you're getting close to undecidability in a device driver, it's not a good thing.
Doesn't the fact that it includes an "Inconclusive" category pretty much mean that it absolutely does not try to solve the halting problem?
The halting problem doesn't state that you can never determine if any specific algorithm halts or not, just that there exists some algorithms which will be inconclusive for any finite bound on the time used to determine if it halts or not.