Comment by kiriakasis

In this case the bootstrapping problem is slightly different. What you are bootstrapping is not the compiler but the verification, in coq this would be trusting that the ocaml extracted code is correct by the coq proofs.

But I might be wrong, there are a lot of nuances and I do not know them all...