<div dir="ltr"><div>Hi Yotam,</div><div><br></div><div>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 (<a href="https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs">https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs</a>). It even has an independent typechecker for internal syntax (<a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/CheckInternal.hs">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/CheckInternal.hs</a>).</div><div><br></div><div>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 (<a href="https://dl.acm.org/citation.cfm?doid=3243631.3236770">https://dl.acm.org/citation.cfm?doid=3243631.3236770</a>) 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...).</div><div><br></div><div>Another important part of Agda's trusted core is the conversion checker, which in Agda shares most code with the constraint solver (<a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion.hs">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion.hs</a>), 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 (<a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion/Pure.hs">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion/Pure.hs</a>).</div><div><br></div><div>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.</div><div><br></div><div>All the best,</div><div>Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Dec 3, 2019 at 6:05 PM Yotam Dvir <<a href="mailto:yotamdvir@mail.tau.ac.il">yotamdvir@mail.tau.ac.il</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;">Hi there,<div><br></div><div>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><br></div><div>Is this understanding correct?</div><div>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><br></div><div>(You are also welcome to answer <a href="https://cstheory.stackexchange.com/q/45665/54969" target="_blank">on cstheory.stackexchange</a>.)</div><div><br></div><div>Thanks in advance!</div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>