pardo@june.cs.washington.edu (David Keppel) (01/07/89)
unido!gmdzi!jc@uunet.uu.net (Juergen Christoffel) writes: >[How do you prove the prover? (e..g, how can we > be confident that the prover is itself correct)] Several answers: * If the prover proves an arbitrary specification, then we prove the prover trivially once we've built it. Consider a C compiler that is written in C and which illustrates the programs that it compiles. (An illustrated program is one that shows you graphical views on the internal data structures of the program. Better descriptions and references on requests). Once we have an illustrating compiler, it is trivial for the compiler to illustrate itself. * ``Perfect'' proofs are not necessary if the prover tells us what it *didn't* do. Thus, the prover need not be complete. (This view may be unpopular with some. By analogy, I believe that a compiler should do what it does very well and that it is ok if I have to write context-swap code by hand). If we could automatically prove that certain parts of a program are correct, then we are still ahead of where we are right now. Things that are especially important to get correct will be written so that they are more amenable to a prover. It *is* important for the prover to identify those things that it can't prove. * Confidence through repeated use: even if parts of the prover remain unproven, there is a measure of confidence in the result, since the prover has been used ("successfully") to prove some number of other programs. Good code that the prover ``proves'' wrong will be detected fairly easily. Bad code that isn't proven incorrect will be harder to track down, since we may have to wait until a ``proven'' program crashes to identify something that the prover didn't get right. The moderator writes: >[Based on other standards, I'm skeptical that any non-trivial program > could have a bug-free specification, given current formalisms.] Put another way, a perfect prover shows that the specification and the code match, but doesn't show that the program is *correct*. Agreed. But there is a lot that *is* amenable to proof. Consider a common argument for using HLLs: ``The complexity of most code is best managed by machine. Spend 90% of your time worrying manually about the 10% of the code that is most important, let the compiler take care of the rest''. This same kind of argument can be applied to proofs. If I want to prove that my sort routine is stable, then I need to prove that it is a sort and that the sort is stable. It might be easy for me to state formally that the results are sorted and have my prover show that it is a sort. It might be that (for some reason) the prover can't show that my sort is stable. That's still better than forcing me to do it *all* by hand, since the part that is ``hard'' to me may be ``easy'' for the machine. Also, I'll have more confidence in the proof by the machine than in my own (hand) proof, since humans make bugs in proofs much as they make bugs in the code they're trying to prove. (Thanks to Richard Fateman for pointing this ``obvious'' fact out for me.) Finally, to use another compilers argument, ``Focus on clarity. As the optimizer matures, the machine-generated optimizations will get closer and closer to the hand-optimized version.'' As the prover gains maturity, less and less of a program will need to be proven by hand (or, alternatively, more and more of the program will be proven correct). ;-D on ( Proof by two legs ) Pardo -- pardo@cs.washington.edu {rutgers,cornell,ucsd,ubc-cs,tektronix}!uw-beaver!june!pardo -- Send compilers articles to ima!compilers or, in a pinch, to Levine@YALE.EDU Plausible paths are { decvax | harvard | yale | bbn}!ima Please send responses to the originator of the message -- I cannot forward mail accidentally sent back to compilers. Meta-mail to ima!compilers-request