It's not self-hosted, so it is not yet at the point where the Thompson hack would apply. That is, CompCert is a C compiler, but it's not written in C, it's wri

It's not self-hosted, so it is not yet at the point where the Thompson hack would apply. That is, CompCert is a C compiler, but it's not written in C, it's written in Coq. So when you use it, you have to trust that the Coq implementation was written correctly, and that nobody has inserted any backdoors in Coq which insert backdoors in Compcert which insert backdoors in your program. The next level would be to also have a verified Coq compiler, which would make the whole system that much more trustworthy. And at _that_ point you could worry about self-perpetuating backdoors in that compiler, and ways to mitigate them.