<div dir="ltr"><div>Hi Xuanrui,</div><div><br></div><div>It's very hard to measure because as I said, most parts of Agda's core don't have an independent typechecker, so all the code is mixed up with the elaboration of user code to internal syntax.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Dec 4, 2019 at 10:18 AM Xuanrui Qi <<a href="mailto:xuanrui@nagoya-u.jp">xuanrui@nagoya-u.jp</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">Hi Jesper, Hi Yotam,<br>
<br>
I wonder, how large, in total, are those components that could be<br>
considered part of the "kernel" of Agda? I know that Coq's kernel is<br>
quite large (>10000 lines OCaml), but Agda seems a much lighter system<br>
than Coq so I expect the number to be much smaller?<br>
<br>
Best,<br>
Xuanrui<br>
<br>
On Wed, 2019-12-04 at 10:13 +0100, Jesper Cockx wrote:<br>
> Hi Yotam,<br>
> <br>
> It is true that Agda currently has a much shakier foundation than say<br>
> Coq or Lean. It does have an internal term syntax that could be seen<br>
> as a core language (<br>
> <a href="https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs" rel="noreferrer" target="_blank">https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs</a><br>
> ). It even has an independent typechecker for internal syntax (<br>
> <a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/CheckInternal.hs" rel="noreferrer" target="_blank">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/CheckInternal.hs</a><br>
> ).<br>
> <br>
> However, this story is far from complete because it takes the<br>
> signature of defined types and functions for granted. In particular,<br>
> functions by dependent pattern matching are represented as case trees<br>
> that need to pass coverage checking and termination checking, which<br>
> means those checks are also part of Agda's 'trusted core'. In our<br>
> ICFP paper last year (<br>
> <a href="https://dl.acm.org/citation.cfm?doid=3243631.3236770" rel="noreferrer" target="_blank">https://dl.acm.org/citation.cfm?doid=3243631.3236770</a>) Andreas and I<br>
> describe a potential core language for case trees, but so far there<br>
> is no independent typechecker for case trees as we have for internal<br>
> syntax (one day...).<br>
> <br>
> Another important part of Agda's trusted core is the conversion<br>
> checker, which in Agda shares most code with the constraint solver (<br>
> <a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion.hs" rel="noreferrer" target="_blank">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion.hs</a><br>
> ), while in Coq it's two separate algorithms. Recently I added the<br>
> possibility to run the conversion checker in 'pure' mode which is<br>
> guarateed to be free of side-effects (<br>
> <a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion/Pure.hs" rel="noreferrer" target="_blank">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion/Pure.hs</a><br>
> ).<br>
> <br>
> As you can see, there is bits and pieces that could be part of a core<br>
> language of Agda, but no real coherent story yet. In general, any<br>
> attempt to build a core language will also be an exercise in<br>
> selecting which features of Agda should be included and which ones<br>
> should not (e.g. irrelevance, sized types, prop, rewrite rules,<br>
> cubical, ...). Yet this selection of various features would've been<br>
> much harder to implement if Agda already had a core language from the<br>
> beginning, so not having a core language has advantages as well as<br>
> disadvantages.<br>
> <br>
> All the best,<br>
> Jesper<br>
> <br>
> On Tue, Dec 3, 2019 at 6:05 PM Yotam Dvir <<a href="mailto:yotamdvir@mail.tau.ac.il" target="_blank">yotamdvir@mail.tau.ac.il</a>><br>
> wrote:<br>
> > Hi there,<br>
> > <br>
> > I am interested in the soundness of Agda as a proof-assistant. To<br>
> > my understanding Agda development veers more in the direction of<br>
> > interesting abstractions and advanced programming features, at the<br>
> > cost of less solid foundations.<br>
> > <br>
> > Is this understanding correct?<br>
> > How close is Agda to having a so-called "small kernel”, and how<br>
> > does it compare to other proof-assistants such as Coq and HOL<br>
> > Light?<br>
> > <br>
> > (You are also welcome to answer on cstheory.stackexchange.)<br>
> > <br>
> > Thanks in advance!<br>
> > _______________________________________________<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>
> <br>
> _______________________________________________<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>
<br>
_______________________________________________<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>