You are right, but this sentence makes sense in the context for which CompCert is intended. The requirements of the DO-178 standard for aeronautics, for instan

You are right, but this sentence makes sense in the context for which CompCert is intended. The requirements of the DO-178 standard for aeronautics, for instance, are such that the choice for compiling safety-critical C code that runs within the aircraft is basically between either: - the equivalent of “gcc -O0”, that is, an off-the-shelf compiler with no optimization so that source-level constructs can be mapped to assembly constructs and vice versa, or - CompCert with optimizations, because the soundness of the optimizations can be justified to a level of formality such that it matters less to be able to trace assembly to source. A source without much detail, but the best I can find within 5 minutes of googling: http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris.pdf http://projects.laas.fr/IFSE/FMF/J3/slides/P05_Jean_Souyiris...