Newsgroups: comp.lang.misc
Path: utzoo!utgpu!watserv1!watmath!tolstoy.waterloo.edu!mhcoffin
From: mhcoffin@tolstoy.waterloo.edu (Michael Coffin)
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr11.161347.26513@watmath.waterloo.edu>
Sender: news@watmath.waterloo.edu (News Owner)
Organization: University of Waterloo
References: <1726@optima.cs.arizona.edu>
Date: Thu, 11 Apr 1991 16:13:47 GMT
Lines: 43

In article <1726@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:
>Can anyone who thinks it is useful to "prove" programs correct provide
>me with an explanation of exactly what the proof accomplishes?  What
>do you know after the proof that you didn't know before the proof?
>Before you answer, consider this: the process of deriving a
>mathematical proof is every bit as prone to errors as is the process
>of writing a computer program.

If I prove a program correct I have a high degree of confidence that
the program will work.  If I both prove it and test it my confidence
is extremely high.  Even then I'm not *certain* that it will work.  I
don't "know" anything after the proof than I knew before, but then I
don't after testing either.  This is especially true of parallel
programs, where nondeterminism makes it notoriously difficult to find
errors by testing.  After testing I suppose I might be said to
"know" at least that the program works on the test input, but even
there I might make a mistake about what the output should be.
Deriving a mathematical proof is error prone, but deriving a proof
*and* a program is certainly less prone to error than just writing a
program. 

>Also consider that when you have written a program, you can test it to
>get some level of confidence that it works.  When you have written a
>proof, the only way to "test" it is to let others read it and try to
>find problems with it.  (Note that "testing" a proof is not the same
>as "testing" a theorem.  You can test a theorem by looking for
>multiple proofs, and by looking for contradictions.)

Why do you set proofs against testing?  Why not do whichever is
appropriate, or do both?  For code that counts the lines in a file,
testing is fine.  For a distributed program that flys an airplane or
monitors my vital signs, both testing and proof are appropriate.

Also, I don't understand the parenthetical comment.  You *can* test a
proof by independently deriving another. (The resulting proof may or
may not be different.) And you *can* test a proof by looking for
counterexamples.  What are you getting at here?

Michael Coffin				mhcoffin@watmsg.waterloo.edu
Dept. of Computer Science		office: (519) 885-1211
University of Waterloo			home:   (519) 725-5516
Waterloo, Ontario, Canada N2L 3G1