[axorb]

>Second, about proof-by-Coq: If there's ever a bug in Coq, they're going to have to re-run all the proofs that have been done this way, and see which (if any) of them are actually invalid. (It still may be better than proof by convincing humans, though...)

I'm no mathematician, but drawing a parallel between the general software world and software-aided mathematical proofs: wouldn't it be natural for a "compiler" to start off by using another technology (in this case, a classic "informal" programming language), and in a later date self-host? I'm saying, couldn't coq reach a state where he could prove itself and the technology stack below him down to axioms?

[digama]

It's already in this state. See Coq-in-Coq, where Coq formalizes its own foundations. Note that this is not entirely convincing, because if Coq was in fact inconsistent then the fact that it could prove its consistency is not surprising. But it is impossible to truly overcome this, and it certainly goes a long way to improve confidence in the system.