Re: Verified compilers?

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

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! ;-)