Path: utzoo!utgpu!watmath!clyde!ima!compilers-sender
From: henry@zoo.toronto.edu (Henry Spencer)
Newsgroups: comp.compilers
Subject: Re: Why Can't We Build a C Compiler?
Message-ID: <3098@ima.ima.isc.com>
Date: 22 Dec 88 01:50:18 GMT
Sender: compilers-sender@ima.ima.isc.com
Reply-To: henry@zoo.toronto.edu (Henry Spencer)
Lines: 23
Approved: compilers@ima.UUCP

>  ... My advisor of days gone by told me ``proofs of
>  correctness, done by humans, anyway, are subject to bugs just like
>  the programs that they are supposed to prove.''  Good point.

Note, in particular, an old but still relevant paper:  "Observations
of Fallibility in Applications of Modern Programming Methodologies",
Gerhart and Yelowitz, IEEE Transaction on Software Engineering, Sept 76.
This study found errors in published programs by folks like Wirth, Naur,
London, and Wulf -- some in programs used as examples of how to prove
correctness!  Considering the unquestionable qualifications of their
authors, the multiple reviews involved in publishing in a textbook or
refereed journal, and the relatively small and tractable problems
attacked, this doesn't exactly fill one with confidence about rigorous
verification of a compiler.  At least, not without extensive software
assistance.

                                     Henry Spencer at U of Toronto Zoology
                                 uunet!attcan!utzoo!henry henry@zoo.toronto.edu
--
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