From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,d1df6bc3799debed
X-Google-Attributes: gid103376,public
From: dewar@merv.cs.nyu.edu (Robert Dewar)
Subject: Re: Not intended for use in medical,
Date: 1997/04/25
Message-ID: <dewar.861973931@merv>#1/1
X-Deja-AN: 237286714
References: <3.0.32.19970423164855.00746db8@mail.4dcomm.com>
 <336c2531.6986514@news.airmail.net>
Organization: New York University
Newsgroups: comp.lang.ada
Date: 1997-04-25T00:00:00+00:00
List-Id: <comp.lang.ada>


Kevin Cline said

<<> My question is, Does validation of an Ada
>compiler on a platform provide significant evidence that the processor
>produces valid object code?

It didn't for Ada-83.  In 1991 I found code generation bgs in both the
validated Verdix compiler and the validated Telesoft compiler.>>

You are answering the wrong question. YES, validatoin provides significant
evidence that the processor produces valid object code, NO it dos not
prove that the processor produces valid object code in all cases.

This is a very important distinction. People tend to rattle bewtween these
two positions:

1. Validation proves that a compiler is completely correct

2. Validation is useless, validated compilers still have bugs

The truth is between, and nicely captured by the "significant evidence"
phrase in the quoted question.