2 ms·
But you didn't answer my point: mathematical errors that escape the original prover are caught by inspection by other mathematicians, and one thing we already k
by gruseom 17y ago
But you didn't answer my point: mathematical errors that escape the original prover are caught by inspection by other mathematicians, and one thing we already know about the software business is that inspection is an extremely scarce resource relative to the amount of code produced.
- jerf 17y agoOh, well: "Verifying the kernel—known as the seL4 microkernel—involved mathematically proving the correctness of about 7,500 lines of computer code in an project taking an average of six people more than five years." Observing that that is not practical was pointed out by Bruce, too. In this case there was a lot of examination. (Frankly, sounds pretty dull to me.)