From: mcsun!cernvax!chx400!sicsun!disuns2!elcgl.epfl.ch!madmats@uunet.uu.net
Subject: Re: Yearly Fees for Support of Compiler
Date: 17 May 91 17:50:35 GMT [thread overview]
Message-ID: <1991May17.185035.1@elcgl.epfl.ch> (raw)
In article <EACHUS.91May14225903@largo.mitre.org>, eachus@largo.mitre.org (Robert I. Eachus) writes:
> I totally disagree when it comes to compilers, no one who knows
> what they are talking about will make any promise of "correctness." In
> fact, any compiler expert will guarentee that ANY compiler that you
> buy will have bugs in it, and in fact will have some errors which
> can't be proven to be errors! (If you don't understand whence this
> comes read Godel, Escher, Bach... and apply the incompleteness theorem
> to compilers.) So, many times, the effect of "support" is known to be
> that "fixing" the compiler so that user X can compile his program,
> means that some user Y will be complaining later that the new version
> of the compiler won't compile his old source file!
>
I disagree here: Goedel, Escher, Bach has nothing to do with Ada compilers at
this level: care was taken in the design of the language not to include
undecidable questions in determining whether or not a given Ada program is
correct or not (see for instance the modifications in the rules on elaboration
of library units from Ada 80 to Ada 83).
What is true, on the other hand, is
- The LRM cannot be proven to be noncontradicotry, because it is not based on a
formal model, among other reasons.
- It cannot be proven that an Ada compiler is fully correct, but it can
certainly be proven that it is wrong in rejecting (or generating wrong code
for) some precise program. If you disagree, please exhibit an Ada program
of which the correctness cannot be decided upon.
When you come to talk about things like "correcting one bug introduces
another", you are talking about the lack of regression testing, and nothing
else.
Mats
next reply other threads:[~1991-05-17 17:50 UTC|newest]
Thread overview: 14+ messages / expand[flat|nested] mbox.gz Atom feed top
1991-05-17 17:50 mcsun!cernvax!chx400!sicsun!disuns2!elcgl.epfl.ch!madmats [this message]
-- strict thread matches above, loose matches on Subject: below --
1991-05-08 18:24 Yearly Fees for Support of Compiler david nash
1991-05-08 19:57 ` Charles H. Sampson
1991-05-09 6:02 ` rharwood
1991-05-09 14:25 ` Jerry Callen
1991-05-09 16:05 ` Drew Johnson
1991-05-14 22:59 ` Robert I. Eachus
[not found] <172546@<1991May3>
1991-05-07 14:26 ` stt
1991-05-08 18:44 ` Kevin Simonson
1991-05-09 7:28 ` Jim Showalter
1991-05-09 20:07 ` Charles H. Sampson
1991-05-10 5:59 ` Jim Showalter
1991-05-12 22:00 ` Erik Naggum
1991-05-16 14:52 ` David T. Lindsley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox