[Agda] Small Kernel

[Xuanrui Qi]

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