<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Xuanrui,<br>
<br>
But it would probably be fair to say (I think?) that if we were to
count, it would be extremely surprising if Agda's core turns out
to be lighter than Coq's. Much of the apparent weight of Coq is in
the tactic language, various typeclass mechanisms etc, which are
distinctly not part of the kernel.<br>
<br>
Best,<br>
<br>
Arjen<br>
</p>
<div class="moz-cite-prefix">On 12/4/19 10:35 AM, Jesper Cockx
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAEm=boyHMg1GAvjr1fXY9p40bFEK-Q3_5X0zKp+3cPZG3H8Twg@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<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"
moz-do-not-send="true">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" moz-do-not-send="true">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" moz-do-not-send="true">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" moz-do-not-send="true">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" moz-do-not-send="true">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" moz-do-not-send="true">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"
moz-do-not-send="true">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" moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
> > <a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
> <a
href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>