>>8 there is none, and never will be (at least, not one which doesn't have the same problem), but i don't think that's so important - exploiting interpreter bugs to prove false generally is a very deliberate action, and proofs (to this point) are generally written by people who want, above all, to know that their own code is correct, and so are unlikely to take deliberate actions to prove their theorems using compiler bugs, not to mention the risk of being found out upon future interpreter updates (that might fix the bug they used to prove false). so i think that even if you can't prove coq correct, theorems proven in it are still very trustworthy, at least if they're not made by hostile entities (NSA writing a proof of a crypto implementation, for example)

there is none, and never will be (at least, not one which doesn't have the same problem), but i don't think that's so important - exploiting interpreter bugs to prove false generally is a very deliberate action, and proofs (to this point) are generally written by people who want, above all, to know that their own code is correct, and so are unlikely to take deliberate actions to prove their theorems using compiler bugs, not to mention the risk of being found out upon future interpreter updates (that might fix the bug they used to prove false). so i think that even if you can't prove coq correct, theorems proven in it are still very trustworthy, at least if they're not made by hostile entities (NSA writing a proof of a crypto implementation, for example)