# Small kernel (i.e. proof-verifier) for Agda?

Proof-assistants usually include a lot of machinery that assists in the creation of proofs. The creation process may be unsound without risking the soundness of the proof-assistant if the alleged proof that was created is later verified by a sound proof-verifier. The smaller this verifier is, the less likely it is to be unsound due to coding or reasoning errors. The term small kernel was coined to refer to such a verifier in Barendregt and Geuvers (the idea apparently goes back to De Bruijn).

I have found literature mentioning this concept in relation to Coq and HOL Light (among others), but not to Agda, hence the question:

How close is Agda to having a small kernel? How does it compare to other proof-assistants such as Coq and HOL Light?

Geuvers, H., Proof assistants: history, ideas and future, Sādhanā 34, No. 1, 3-25 (2009). ZBL1192.68629.

Barendregt, Henk; Geuvers, Herman, Proof-assistants using dependent type systems, Robinson, Alan (ed.) et al., Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/ Elsevier; 0-444-50812-0 (vol. 2); 0-444-50813-9 (set)). 1149-1238 (2001). ZBL1005.03011.

Adams, Mark, Proof auditing formalised mathematics, ZBL07106502.

• You'd better off asking this question on the Agda mailing list. – Andrej Bauer Oct 11 at 7:41