<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi there,<div class=""><br class=""></div><div class="">I am interested in the soundness of Agda as a proof-assistant. To my understanding Agda development veers more in the direction of interesting abstractions and advanced programming features, at the cost of less solid foundations.</div><div class=""><br class=""></div><div class="">Is this understanding correct?</div><div class="">How close is Agda to having a so-called "small kernel”, and how does it compare to other proof-assistants such as Coq and HOL Light?</div><div class=""><br class=""></div><div class="">(You are also welcome to answer <a href="https://cstheory.stackexchange.com/q/45665/54969" class="">on cstheory.stackexchange</a>.)</div><div class=""><br class=""></div><div class="">Thanks in advance!</div></body></html>