You are talking about high-assurance code, which is roughly a statistical classification regarding failure rate. Pron is talking about formal verification, whi

You are talking about high-assurance code, which is roughly a statistical classification regarding failure rate. Pron is talking about formal verification, which proves something to be correct according to a mathematical model. Formal verification is not required to produce code with a very low failure rate. I have personally known about unpatched vulnerabilities worth a small fortune which were not exploited because most people who chose to become programmers aren't assholes, or at least not criminally so. Formal verification is not a magical certification that software is bug free, as there will inevitably be an error in the specification itself or how the specification relates to the hardware. This is astonishingly rare, however, I think Coq has had a single major error in the TCB. The space shuttle, various nuclear accidents, and plain old manufacturing are example on the limits to which engineering can prevent failure: we just can't shove the real world into statistical models. You two are in agreement, but seem to be talking past each other :(