He also points to Compcert: a certified compiler for a subset of C. The compiler is specified, programmed and proved in Coq. It is a really impressive project: http://compcert.inria.fr/compcert-C.html