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

Question

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.

Answer 1

It is true that Agda currently has a much shakier foundation than say Coq or Lean. It does have an internal term syntax that could be seen as a core language (https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs). It even has an independent typechecker for internal syntax (https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/CheckInternal.hs).

However, this story is far from complete because it takes the signature of defined types and functions for granted. In particular, functions by dependent pattern matching are represented as case trees that need to pass coverage checking and termination checking, which means those checks are also part of Agda's 'trusted core'. In our ICFP paper last year (https://dl.acm.org/citation.cfm?doid=3243631.3236770) Andreas and I describe a potential core language for case trees, but so far there is no independent typechecker for case trees as we have for internal syntax (one day...).

Another important part of Agda's trusted core is the conversion checker, which in Agda shares most code with the constraint solver (https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion.hs), while in Coq it's two separate algorithms. Recently I added the possibility to run the conversion checker in 'pure' mode which is guarateed to be free of side-effects (https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion/Pure.hs).

As you can see, there is bits and pieces that could be part of a core language of Agda, but no real coherent story yet. In general, any attempt to build a core language will also be an exercise in selecting which features of Agda should be included and which ones should not (e.g. irrelevance, sized types, prop, rewrite rules, cubical, ...). Yet this selection of various features would've been much harder to implement if Agda already had a core language from the beginning, so not having a core language has advantages as well as disadvantages.