I felt like that was kind of misleading when I read that section. Compcert is hardly an optimizing compiler compared to GCC. And bugs were found in it (just no

I felt like that was kind of misleading when I read that section. Compcert is hardly an optimizing compiler compared to GCC. And bugs were found in it (just not middle end). It's unclear to me how the defect rate really compared for equivalent performance code (which is probably -O0 or maybe -O1 gcc). CompCert also had correctness as a headline goal in a way that other compilers have not, so because of these differences it's hard to tell how much impact formal methods were themselves have. Though it its reason to be hopeful at least.