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=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,5412c98a3943e746
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.74.201 with SMTP id w9mr1666206pbv.0.1330073579391;
        Fri, 24 Feb 2012 00:52:59 -0800 (PST)
Path: 
 h9ni3131pbe.0!nntp.google.com!news2.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!de-l.enfer-du-nord.net!feeder1.enfer-du-nord.net!usenet-fr.net!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Fri, 24 Feb 2012 09:52:58 +0100
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6;
 rv:8.0) Gecko/20111105 Thunderbird/8.0
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: Re: Verified compilers?
References: <op.v91cleyiule2fv@douda-yannick>
 <078983c8-845c-41d3-99e1-08968e9a1a9a@q12g2000yqg.googlegroups.com>
In-Reply-To: 
 <078983c8-845c-41d3-99e1-08968e9a1a9a@q12g2000yqg.googlegroups.com>
Message-ID: <4f474fea$0$6628$9b4e6d93@newsspool2.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 24 Feb 2012 09:52:58 CET
NNTP-Posting-Host: 7f470204.newsspool2.arcor-online.net
X-Trace: 
 DXC=<Y0LR^ihc[]aoembcbF;DQA9EHlD;3YcR4Fo<]lROoRQ8kF<OcfhCO[\M8Q7Z_Bh2]PCY\c7>ejVX55jCb\o4hRX\T0a7c;k^fR
X-Complaints-To: usenet-abuse@arcor.de
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2012-02-24T09:52:58+01:00
List-Id: <comp.lang.ada>

On 24.02.12 02:41, Shark8 wrote:

> I think the sentence shows a bit of solipsistic thinking on the part
> of the writer's view of languages; as everyone on this thread ought to
> know Ada's had verified compilers since its first implementations. (I
> am using 'verified' and 'certified' rather interchangeably here, if
> that's not the case though I'd like to hear what exactly the
> difference is.)

http://compcert.inria.fr/doc/

"Compcert is a compiler that generates PowerPC, ARM and x86 assembly
  code from Compcert C, a large subset of the C programming language.
  The particularity of this compiler is that it is written mostly
  within the specification language of the Coq proof assistant, and
  its correctness --- the fact that the generated assembly code is
  semantically equivalent to its source program --- was entirely
  proved within the Coq proof assistant."

The part saying

"the generated assembly code is semantically equivalent
  to its source program"

is the good bit. A result very different from a compiler's output
passing some test suite.

However, formal verification does not address the qualities of
the semantics, unless it does change the semantics of (the subset
of) C:
Whether or not a project will profit, then, from the
semantics of C's int, be it in C source text or in assembly code,
is unrelated to the formal verification of the translation,
I should think. The qualities of C's semantics would now be
verified to be inherent in C, though, and will be truthfully
reflected by the assembly code! ;-)