Arto's Notes re: CompCert

CompCert is a formally-verified C99 compiler.