We introduce a notion of program equivalence between different
languages and talk about what kind of mathematical techniques are
used, how it gives a compositional notion of compiler correctness and
more ambitiously how it may be seen as a technique to prove the
correctness of programs. We also briefly discuss how these ideas
can be formalized and verified in the formal proof assistant Coq.