Lots of people in this thread are complaining that a formal proof is not reasonable and will not catch all classes of errors. I think r00fus is right to look a

Lots of people in this thread are complaining that a formal proof is not reasonable and will not catch all classes of errors. I think r00fus is right to look at the profit motive of the software supplier. Microsoft would have been climbing a steep curve of diminishing returns for basically no extra revenue. Windows isn’t the monster revenue generator and in the server space it’s losing to free Operating Systems. We ask for perfect security but we as an industry/market aren’t willing to pay the premium to go from “it mostly does what I want most of the time” to “life critical with near perfect security”. That said, I don’t think regulation would work here and I suspect there would be a perverted incentive by the regulator if an issue was found (like in this case where government, military, and critical industry get early access to the fix).