If I remember correctly the problem Thompson described is tougher to deal with than this. Yes, the CompCert compiler is certified, but the problem is that the compiler that bootstrapped CompCert may not be. If you use some compiler (let's call it gccb, for backdoored gcc) to bootstrap CompCert that outputs ccb (backdoored compcert). Now you recompile CompCert with ccb since CompCert is certified. This gets you a final version of CompCert compiled with a bootstrapped CompCert. So the process is gccb -> ccb -> cc. But then the backdoor has just been transmitted down the line to cc.

Edit: also I just looked and it appears that CompCert is written in OCaml. This doesn't substantively change anything above. It just means that rather than having a backdoored gcc you'd have a backdoored ocamlc.

Realistically the only way to truly assure that your compiler is not backdoored is by writing it yourself in assembly. But then, your assembler might be backdoored. So you need to write your own assembler in binary. But then your processor might be backdoored. So you need to design your own processor. And then you might be safe. Of course, if someone really cared enough to backdoor all that stuff, they'd probably just come after you with a rubber hose at that point. And I think that was the point Thompson was trying to make.