I have a simple question. Can we prove that a compiler is correct? I
mean we are given a language with it's syntax and semantics and a
compiler whose correctness needs to be proved. Is this theoretically
possible?

Yes, it is. In the PPL 2006 conference proceedings, Xavier Leroy
reported on his efforts implementing a provably-correct compiler for a
subset of C.

The proof is extremely large, however, and in order to ensure the
proof's correctness he had to develop the compiler in a theorem
proving system that verified the correctness of all his proofs.

"Formal certification of a compiler back-end, or: programming a
compiler with a proof assistant"

<http://pauillac.inria.fr/~>

Neelakantan Krishnaswami wrote:
>I have a simple question. Can we prove that a compiler is correct? I
>mean we are given a language with it's syntax and semantics and a
>compiler whose correctness needs to be proved. Is this theoretically
>possible?
>
Yes, it is. In the PPL 2006 conference proceedings, Xavier Leroy
reported on his efforts implementing a provably-correct compiler for a
subset of C.

The proof is extremely large, however, and in order to ensure the
proof's correctness he had to develop the compiler in a theorem
proving system that verified the correctness of all his proofs.

"Formal certification of a compiler back-end, or: programming a
compiler with a proof assistant"

<http://pauillac.inria.fr/~>

[Interesting paper. I wonder how likely it is that the tools, which
are not small, or the set of axioms have bugs that could affect the
validity of the proof. If it sounds like I'm channelling the famous
1979 proof paper by Perlis et al, it's not surprising since he was my
thesis advisor. -John]

A lot of the design of these tools has been shaped in specific
response to Perlis's paper.

Basically, the idea is that a theorem prover is inherently
untrustworthy. It's large, complex, and relies on very advanced math
for its correct operation -- it will have bugs with basically 100%
certainty.

So what these programs do is construct the actual proof of the theorem
as a data structure which you can print out. Then, you can write a
proof *checker* to verify the operations that the theorem prover has
carried out.

A proof checker is much smaller than the theorem prover; usually they
are a few hundred lines of code. Thus, they are small enough that
Perlis's criticisms don't apply to them -- the checkers are programs
that people can manually verify and easily write multiple competing
implementations to increase trust.

So, the process is:

1. You develop your proof interactively with the prover.
2. You dump out the proof and run your proof checkers on it.
3. If it says your proof is good, then you're done.
4. If it says your proof is bad, then you curse, and fix the
bug in the theorem prover and redo your proof.

Interestingly, this is a technique that Leroy used in his compiler.
For example, the register allocator would find a coloring, and then
he'd run a checker on it to ensure that it was okay before proceeding.
If the check failed, then his compiler would report that it failed to
compile that program rather than emitting incorrect code.

IIRC, the logic in Coq is equivalent to ZFC with countably many
inaccessible cardinals. That's a very rich foundation, but still
pretty conventional.

our moderator writes:
>[Interesting paper. I wonder how likely it is that the tools, which
>are not small, or the set of axioms have bugs that could affect the
>validity of the proof

Also relevant -- although not quite the same thing -- is George Necula's
work on "certifying compilers" (e.g. his PLDI98 paper). Here the idea is
not to prove the compiler correct, but to prove its *output* correct, in
at least limited respects.

The idea is that the compiler annotates the output code with a proof that
the code satisfies certain constraints. That proof is then checked by an
independent checker -- *much* smaller and simpler than a theorem prover.
The result is that you can trust the compiler's output to have certain
properties even if you're not sure the compiler itself is correct. (He
also found it a very effective tool for compiler debugging.)

Neelakantan Krishnaswami <neelk@cs.cmu.eduwrote:

Basically, the idea is that a theorem prover is inherently
untrustworthy. It's large, complex, and relies on very advanced math
for its correct operation -- it will have bugs with basically 100%
certainty.

So what these programs do is construct the actual proof of the theorem
as a data structure which you can print out. Then, you can write a
proof *checker* to verify the operations that the theorem prover has
carried out.

This is interesting, because, in working on a theorem prover, I have
reached the same conclusions. Particularly, the question of bound
variables is tricky.

I think, though, one might combine a theorem prover and a proof
checker, so that the faulty proofs are detected right away. This is
what I am about to do, at least. Roughly, what is needed, is that
the*substitutions that the theorem prover engine (think of Prolog, but
more complicated) discovers are then verified for correctness.

A proof checker is much smaller than the theorem prover; usually they
are a few hundred lines of code. Thus, they are small enough that
Perlis's criticisms don't apply to them -- the checkers are programs
that people can manually verify and easily write multiple competing
implementations to increase trust.

example of a small, standalone one is MetaMath
<http://us.metamath.org/>. A mathematical proof consists essentially
of finding suitable*substitutions applied to a suitable sequence of
axioms which leads up to the statement one wants to prove. So all the
proof checker needs to do is that the found sequence of axioms (and
formerly proved statements, as they can be formally expanded) and
substitutions are applied correctly.

So, the process is:

1. You develop your proof interactively with the prover.
2. You dump out the proof and run your proof checkers on it.
3. If it says your proof is good, then you're done.
4. If it says your proof is bad, then you curse, and fix the
>* * bug in the theorem prover and redo your proof.

I think the point 4 here is very important. :-) It is very difficult to
develop a bug-free theorem prover.

Interestingly, this is a technique that Leroy used in his compiler.
For example, the register allocator would find a coloring, and then
he'd run a checker on it to ensure that it was okay before proceeding.
If the check failed, then his compiler would report that it failed to
compile that program rather than emitting incorrect code.

Therefore, if one would want to do a compiler verifier, one might be
better off to isolate a smaller, algorithmic language, which is easier to
implement a bug-freer one.

IIRC, the logic in Coq is equivalent to ZFC with countably many
inaccessible cardinals. That's a very rich foundation, but still
pretty conventional.

The consistency of ZFC and similar set theories cannot be proved (by
Goedel theorems) unless one invokes a more powerful metamathematics. And
if it is not consistent, all mathematics falls, due to the excluded third
(all statement true all false). then ends up on a belief that the
axioms are sufficient, because what should be used to prove
the*metamathematical theory one invokes to prove these theories? - To do
that, one has to invoke a still more powerful metametamathematics, and so
on. In addition, some mathematical fields require extensions of ZFC
(typically in category related fields). So, one should not assume that ZFC
is a blessing for "all known mathematics", as is a popular belief, it
seems.

Most working math is likely to be constructible within a much smaller
theory than ZFC and such similar axiomatic set theories, as one usually
has some rather basic*explicit objects at the very bottom, by which the
theoretical extensions just come in as tools to be able to handle this in
an efficient manner. And the*algorithmic parts used in a compiler should
be even smaller, just dealing with some rather explicit binary number
manipulations.

So, again, for a compiler verifier, perhaps ii helps focusing on a smaller
theory.

"Daniel C. Wang" <danwang74@gmail.comwrote:

A minimal proof verifier is 1-2 thousand lines of C code. This proof
verifier uses no library calls. It's designed so you can compile it to
assembly and can eyeball the output of the compiler. The basic logic
has around 10 axioms from which all of modern mathematics can be
derived.

I did not know that mathematicians had agreed on a set of axioms from
which all known mathematics can be derived. :-) Would you mind
specifying these axioms?

Further, a theorem prover as MetaMath <http://us.metamath.org/does
not use the Hilbert axioms straight off as written, but a
modification, and does not specify in exact what manners there results
a mathematical difference, if one. Perhaps it is not known.
problem in the context, is that the metamathematical axioms are often
written as*infinite sets of axioms, which in a computer context must
be properly rewritten as substitution axioms. The details here, seems
to be glossed over.

Sid Touati <Sid.Touati@inria.frwrote:
>As example, suppose that the compiler executes on a 32 bits machine and
generates a code for a 64 bits machine. If the compiler makes static
>constant propagation, it makes arithmetic computation on the 32 bit
>machine. This would not give you the same result if you generate the
>code on the 64 bits machines.

Any cross-compiler which doesn't emulate the *target* machine's arithmetic
when performing operations like constant propagation is simply broken.

course, if it does emulate, there is still the issue of whether it
emulates *correctly*. But this is just another case of "are there bugs in
the compiler?"; it's not a fundamental problem of missed assumptions.

>We can imagine more complex cases with floating point computations

Emulating another machine's floating point is definitely a lot of work
(the widespread consensus on IEEE-standard floating point has helped but
doesn't entirely solve the problem). But if you signed on to write a
cross-compiler, well, you knew the job was dangerous when you took it. :-)

Sid Touati <Sid.Touati@inria.frwrites:

I didn't read its last PPL article yet, but I remembered one of his
talks about this subject (certifying a simple compiler). At that time, I
noticed the following hole in their proof. []
Such code optimization has been proved correct by coq, but an
informal assumption has been forgotten. Indeed, the machine
executing the compiler may be distinct from the machine executing
the final generated code. This is the case of cross compilers for
example.

There is no hole of that kind in my compiler proof. The compiler
implements its own 32-bit integer arithmetic, as Coq functions that
are proved to satisfy all the arithmetic and logic properties that the
compiler optimizations rely on (associativity, distributivity,
multiplication by power of 2 is a left shift, etc). This arithmetic
is completely independent of that of the processor executing the
compiler.

These arithmetic operations are used both during compilation (e.g. the
constant propagation phase you mention) and in the formal semantics
for the target processor. That's what ensures that constant
propagation preserves semantics. If const.prop. were to use a
different arithmetic than the target processor, Coq would of course
reject the proof.

Now, you can have doubts that the arithmetic used by the compiler
matches that implemented by the target compiler. This comes back to
the issue raised by other posters in this thread, namely that the
formal semantics for the source language and the target processors
have not been formally proved correct, but only validated informally
by careful reading and by testing. (This is still much easier than
validating a whole compiler using these informal approaches.)

Formal validation of the semantics is possible, e.g. for the target
processor by relating it to the formal models used by processor
manufacturers to verify their chips. Unfortunately, such formal
models of hardware are generally trade secrets, so this is beyond the
scope of my compiler certification project.
- Xavier Leroy

Marco van de Voort <marcov@stack.nlwrote:
>FPU operations are also a can of worms. This e.g. due to additional
>precision in, at least x86, CPUs and the related rounding when saving
>to mem, the outcome of FPU operations is also dependant on the path.
>So result:=x*y*z is different from a1:=x*y result:=a1*z (if a1 is a memory
>location)

Not always. It *is* tricky to do floating-point constant folding, but
there are cases where it can be done, and it is possible to
automatically determine whether it's possible for a particular
expression.

Notably, if both the compiler and the target use IEEE arithmetic, and
you evaluate an expression in the compiler -- including format
conversions and roundings where appropriate -- and evaluation causes
*no* floating-point flags to be raised (not even the Inexact flag),
then it can be evaluated at compile time and moreover it is
independent of rounding mode(*). For example, folding `5.0 * 10.0' to
`50.0' is verifiably safe.

(* With one small exception that you have to watch for: for a finite
X, X-X is always zero, but whether that's +0 or -0 depends on the
rounding mode. There are only one or two situations where it makes a
visible difference. )

You may be able to go farther than that if the language spec permits,
e.g. by allowing inexact constant folding provided rounding is
correct.

Note that I said "both the *compiler* and the target", not "both the
*host* and the target". Compilers can quite reasonably use software
floating point to be sure that they match the exact behavior of the target
machine -- it's not like they do enough compile-time floating-point
arithmetic that its performance is likely to be a problem.

Hans-Peter Diettrich <DrDiettrich@compuserve.dewrote:
>Ambiguities also can arise from different models or precision, as
>implemented in specific FPU hardware. Doesn't this imply that a correct
>compiler must emulate all floating point operations, so that the output
>does not depend on the host machine of the compiler?

Not *necessarily*, although (as I said in a previous message) that may be
a sensible thing to do on general principles.

IEEE floating point, in particular, is sufficiently tightly specified and
sufficiently widely used that a careful cross-compiler running on an IEEE
machine could mostly use its host floating-point hardware to emulate the
floating point of many target machines. (It might have to resort to
software emulation in some tricky areas.)

>The operation of the Intel coprocessor (x87) is configurable, and this
>configuration can be changed at runtime.

That's true of IEEE FPUs in general, not just the x86 one.

>In this case a "correct" compiler has to assure that, after every
>call to external code, the FPU configuration is restored to the
>expected state.

Indeed so. Modern language definitions increasingly are specifying the
details of where FPU state changes, which state changes propagate into and
out of a called routine, etc. With an older language spec, there's room
for implementer judgement about how things should work, but that's no
different from many other areas.