[Agda] Small Kernel

[Jesper Cockx]

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
> <https://cstheory.stackexchange.com/q/45665/54969>.)
>
> Thanks in advance!
> _______________________________________________
> 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/ca7cade8/attachment.html>