This removed the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel.
Αυτό απομάκρυνε την ανάγκη να εμπιστευτούμε τα διάφορα προγράμματα υπολογιστή που χρησιμοποιούνται για να επιβεβαιώσουν συγκεκριμένες υποθέσεις· απαιτείται μόνο να εμπιστευτούμε τον πυρήνα Coq (Gonthier 2008).