Re: More reliable compilers (of some programming langauges) than GNAT

[Paul Rubin <no.email@nospam.invalid>]

Robert Eachus <rieachus@comcast.net> writes:
> The problem is that for some recursive functions, it is not possible
> to prove that the input to the compiler (in Ada) and the output (in
> machine language) compute the same function for some partially
> recursive functions.

That makes no sense at all.  It's in general not possible to prove two
arbitrary programs produce the same output.  The input and output of the
Ada compiler are not arbitrary, but in fact they are closely related, so
nothing gets in the way of such a proof.  Look at CompCert
(compcert.inria.fr) for something like that being done with a C
compiler.  It would be great to use a similar approach for Ada.