4 ms·
Proving correctness isn't enough. You have to test it too. It's perfectly possible for the proof to have errors (bugs). It's also possible for the proof to be i
by SAI_Peregrinus 9y ago
Proving correctness isn't enough. You have to test it too. It's perfectly possible for the proof to have errors (bugs). It's also possible for the proof to be incomplete: you can prove the algorithm is correct and implemented correctly to spec and still have vulnerabilities.
- loup-vaillant 9y agoWhile 100% confidence is impossible (because I'm Bayesian), machine checked proofs do help. It's then a matter of cost/benefit.
- NoGravitas 9y ago"Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth