In this talk, we first give a quick overview of the Coq
system in order to present its trusted computing base. Then,
we present several practical attempts to extend the system
in a trustful way. Finally, we try to draw some conclusions
out of these different attempts.