From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.5-pre1 (2020-06-20) on
	ip-172-31-74-118.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=3.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.5-pre1
Date: 17 May 91 17:50:35 GMT
From: mcsun!cernvax!chx400!sicsun!disuns2!elcgl.epfl.ch!madmats@uunet.uu.net
Subject: Re: Yearly Fees for Support of Compiler
Message-ID: <1991May17.185035.1@elcgl.epfl.ch>
List-Id: <comp.lang.ada>

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