Pieces of software like OS kernels and browsers run code quadrillions upon quadrillions of times per day and yet still suffer hundreds, if not thousands of crit

Pieces of software like OS kernels and browsers run code quadrillions upon quadrillions of times per day and yet still suffer hundreds, if not thousands of critical security vulnerabilities. Testing only demonstrates the presence of bugs, not the absence. There's a whole field of high-assurance software, with verification, formally-proven compilers with translation validation. Only there is there hope that one can write software and prove it, with a machine-checked proof, correct. Tesla is not that far. Not even close. But no matter, let's just deploy it anyway.