I think that really trivializes the tremendous effort the CompCert team put into that work. You don't just need to write a C compiler, or learn a bit of a proof

I think that really trivializes the tremendous effort the CompCert team put into that work. You don't just need to write a C compiler, or learn a bit of a proof assistant, you need to do the actual work of proving the compiler correct. This took person-years of time from people who already were Coq experts.