Coming from a practical angle (i.e., not discussing the limits on logic that we know about due to the incompleteness theorem etc), your question might be rephrased as "Can we do all of the math that we do on paper, in Coq?"
The answer is "Dunno, it's tough. We'll get back to you." You're not the first person to think so though, and there are efforts to "put math on computers". Check out Homotopy TT.
To elaborate a bit: The main reason is that a large portion of mathematics is done using set theory as the working foundation, but set theory is not amenable to being expressed with computers. It's too declarative. The internal logic in Coq (Calculus of Co-inductive Constructions) is based on Martin-Löf Type Theory, which is a quite a different kettle of fish. So some definitions, although equivalent, aren't the same, and some of the low level stuff is not built up in the same way.
Widening the gap between the paper and machine worlds is that there is a preference for Constructive Math in the machine world. (oversimplifying: a preference for not using the law of excluded middle (or equivalent classical axioms/rules)) and intuitionistic logic.
Addendum: What I've been talking about above is how the logical foundations of coq are different from traditional foundations. That said, Coq is still doing math, that requires logical foundation, that is still subject to the limitations of formal logic. The incompleteness theorems etc.
P.S. - No physical computer system can by guaranteed bug free by mathematics. Even if your hard and software is verified, cosmic radiation/favourite energy source may cause bits in your machine to flip and all your verification goes out the window. Even with verification, some programs should be run in triplicate.