Date: Tue, 30 May 2000 22:37:54 -0600 From: ksvhsoft@xmission.com (Kevin S. Van Horn) I'm not proposing to prove correctness for everything. Nor am I proposing a 100% formal, machine-checkable proof. I rarely do correctness proofs myself, but every once in a while I run up against something tricky where it's very difficult to be sure you have it right by just doing operational reasoning. That's when a correctness proof, or mathematical derivation of the algorithm, can be indispensable. I agree. I do the same thing. > It's easy to write code which appears to be proven correct, > only to discover that the code does not actually meet the assertions. > This is most likely in cases such as the multi-thread synchronization > which you mention, in which error cases arise very rarely so > executable assertions are no guarantee of correctness. It seems to me that you're getting proofs and testing mixed up. The whole point of a proof is that it doesn't matter how rare the case is, you still have to account for it or your proof is incomplete. And often it's a lot easier to see that you're missing a piece of your proof than it is to write exhaustive tests. My point is that nothing forces the proof and the code to be identical. Even if the proof is correct, the code may still be incorrect. I mentioned executable assertions because many people use those as part of proving code to be correct, in an attempt to make the proof and the code as identical as possible. I personally don't find it any easier to see that I am missing a piece of a proof than to write exhaustive tests. The most common case in which I use proofs is to make sure that complex data structure manipulations maintain invariants. Ian