Why Writing Correct Software Is Hard and Why Math (Alone) Won’t Help Us [video]
Oh, another halting problem argument.<p>He&#x27;s quite correct that you can write programs for which there&#x27;s no faster way to find out if they halt than running them.  His example is one that tests Goldbach&#x27;s conjecture by brute force. A more practical example is trying to break a crypto key by brute force trials.  Or a Bitcoin miner.<p>His analysis applies to the worst case. Most programs aren&#x27;t like that.  If your program is that close to undecidability, you probably need some kind of a loop counter to keep it under control.<p>Microsoft has a Static Driver Verifier for Windows kernel drivers. It&#x27;s a formal proof of correctness system using symbolic execution. It tests whether a driver will halt (return, really), call any of the driver APIs incorrectly, or violate the execution model by subscripting out of range, using a bad pointer, or other crash-type error. It doesn&#x27;t try to verify that the driver will run the device correctly, just that it won&#x27;t take the entire kernel down.  This is the main reason that driver-caused crashes stopped being a major source of Windows problems in Windows 7 and later. Before the Static Driver Verifier, more than half of Windows crashes were caused by driver bugs.<p>Microsoft&#x27;s experience is that 5% to 10% of the time, the Driver Verifier can&#x27;t decide if a program will get to a bad state.  The Driver Verifier has explored too many cases and gives up. This is usually an indication of a flaky driver.  If the Verifier can&#x27;t tell if the driver will hang, the programmer who wrote it probably can&#x27;t either. So the driver needs to be fixed.  This does not turn out to be a serious problem in practice.<p>(I&#x27;ve worked on proof of correctness systems. There are lots of hard problems, but this just isn&#x27;t one of them.)