Re: Why Can't We Build a C Compiler?

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

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