<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>