Automatic Proofs (WAS: Why Can't We Build a C Compiler?)

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
--

Return to the comp.compilers page.
Search the comp.compilers archives again.