The safety of Coq is a consequence of its consistency, or, better, of the consistency of the calculus of inductive constructions. This follows from the very powerful theorem of strong normalisation, which we also mentioned in the proof theoretical foundations. This is the key to the solution to the de Bruijn principle. All the complexity of the proof of consistency is put into the theorem, which of course is not part of the proof checker. In this way, when we produce a proof object we may pass it to the proof checker, which in this case is just a type checker and it is represented by a trusted, very small piece of code implementing the few typing rules of the calculus of constructions. As a matter of fact, the latest implementations of the type checker are less than 8000 lines long.

---