[Agda] Small Kernel

[Jesper Cockx]

Hi Xuanrui,

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.

-- Jesper

On Wed, Dec 4, 2019 at 10:18 AM Xuanrui Qi <xuanrui at nagoya-u.jp> wrote:

> Hi Jesper, Hi Yotam,
>
> I wonder, how large, in total, are those components that could be
> considered part of the "kernel" of Agda? I know that Coq's kernel is
> quite large (>10000 lines OCaml), but Agda seems a much lighter system
> than Coq so I expect the number to be much smaller?
>
> Best,
> Xuanrui
>
> On Wed, 2019-12-04 at 10:13 +0100, Jesper Cockx wrote:
> > Hi Yotam,
> >
> > 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 (
> >
> https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Internal.hs
> > ). It even has an independent typechecker for internal syntax (
> >
> https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/CheckInternal.hs
> > ).
> >
> > 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 (
> > https://dl.acm.org/citation.cfm?doid=3243631.3236770) 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...).
> >
> > Another important part of Agda's trusted core is the conversion
> > checker, which in Agda shares most code with the constraint solver (
> >
> https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion.hs
> > ), 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 (
> >
> https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Conversion/Pure.hs
> > ).
> >
> > 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.
> >
> > All the best,
> > Jesper
> >
> > On Tue, Dec 3, 2019 at 6:05 PM Yotam Dvir <yotamdvir at mail.tau.ac.il>
> > wrote:
> > > Hi there,
> > >
> > > 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.
> > >
> > > Is this understanding correct?
> > > 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?
> > >
> > > (You are also welcome to answer on cstheory.stackexchange.)
> > >
> > > Thanks in advance!
> > > _______________________________________________
> > > Agda mailing list
> > > Agda at lists.chalmers.se
> > > https://lists.chalmers.se/mailman/listinfo/agda
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191204/97d98a52/attachment.html>