Comment by pseudohadamard

The problem with CompCert is that it produces really bad code, below the level of gcc -O0, about the level of the eternally-in-progress compiler project you worked on in your Programming Languages 370 course. So you can get most of the benefits of CompCert by running a standard compiler with -O0.