This paper sketches a rigorous correctness proof of a compiler
  executable. 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 real machines. Although often left out
  of sight, implementation verification is definitely necessary, not
  only but also for compilers. We will show, that a rigorous compiler
  correctness proof also for the final binary compiler machine program
  is possible and feasible.  Verified compiler implementations
  guarantee correctness properties for generated executable program
  implementations; we need them, not only in safety critical systems,
  but also for security in e.g. network computing.