Re: Reasons why you don't prove your programs are correct

pardo@cs.washington.edu (David Keppel)
22 Jan 90 22:15:02 GMT

          From comp.compilers
Related articles
Reasons why you don't prove your programs are correct steve@hubcap.clemson.edu (1990-01-05)
Re: Reasons why you don't prove your programs are correct keithd@anvil.oz.au (1990-01-12)
Re: Reasons why you don't prove your programs are correct mayer@iuvax.cs.indiana.edu (Mayer Goldberg) (1990-01-17)
Re: Reasons why you don't prove your programs are correct pardo@cs.washington.edu (1990-01-22)
Re: Reasons why you don't prove your programs are correct pardo@cs.washington.edu (1990-01-24)
Re: Reasons why you don't prove your programs are correct gateley@m2.csc.ti.com (1990-01-26)
| List of all articles for this month |
From: pardo@cs.washington.edu (David Keppel)
Newsgroups: comp.compilers,comp.edu
Date: 22 Jan 90 22:15:02 GMT
References: <7578@hubcap.clemson.edu> <1990Jan16.232703.2368@esegue.segue.boston.ma.us>
Organization: University of Washington, Computer Science, Seattle

>[Why don't you prove your programs correct?]


Off-the-cuff reasons:


* Proofs are hard. It's not clear to me that doing proofs is
generally the best use of my time. It *is* clear that there are cases
when it is. Figuring when to and when not to is just one of those
bits of life...


* Proofs are like comments -- easy to leave out.


* People write wrong proofs just like they write wrong programs.


* Proof techniques are not well-integrated. I know of no library
routines that even *claim* to have a formal specification.


;-D on ( Go ahead -- prove my day ) Pardo
--
pardo@cs.washington.edu
        {rutgers,cornell,ucsd,ubc-cs,tektronix}!uw-beaver!june!pardo




Post a followup to this message

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