We're talking proofs here tho, and you aren't allowed to prove something by "throwing enough input at it", isn't it like saying that unit tests are proofs of the correctness of a program?
>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?