This paper sketches our approach to rigorously prove the correctness
of a compiler executable down to its binary machine code
implementation.  We will emphasize the central role of partial
program correctness and its preservation, which capture the
intuitive correctness requirements for transformational programs and
in particular for compilers on realistic machines. Vertical and
horizontal compositionality of L-simulation (preservation of partial
correctness) allows for combining small proof modules to finally
complete the entire proof.  Although often left out of sight,
implementation verification is definitely necessary, not only but
also for compiler programs.  Modularization makes a rigorous
compiler correctness proof also for the final compiler executable
possible and feasible.