what's the largest program you've proved correctness of?
But that's the point. With security code, while you may not prove the correctness of it, there's a black hat that's trying to find a counterexample to your "proof".
Whereas for 99% of proofs that are published in the literature no one is trying to prove that there are flaws in the proof. As someone who reviewed CS papers I would always try to really read at least one proof in the paper. Not skim, but really scrutinize it. Probably 75% of the time I could find a problem with the proof. Usually one that was easily corrected, but it was still wrong. But it took substantial effort to do this (which is why I only did one per paper and just read the other proofs).
Comments
I agree in the abstract, but ...
- what's the largest program you've written? - what's the largest program you've proved correctness of?
So in reality, meaningful proofs are much much much harder than writing programs.
what's the largest program you've proved correctness of?
But that's the point. With security code, while you may not prove the correctness of it, there's a black hat that's trying to find a counterexample to your "proof".
Whereas for 99% of proofs that are published in the literature no one is trying to prove that there are flaws in the proof. As someone who reviewed CS papers I would always try to really read at least one proof in the paper. Not skim, but really scrutinize it. Probably 75% of the time I could find a problem with the proof. Usually one that was easily corrected, but it was still wrong. But it took substantial effort to do this (which is why I only did one per paper and just read the other proofs).
Some recommended reading: http://www1.cs.columbia.edu/~angelos/Misc/p271-de_millo.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/l...