[Agda] Small Kernel

[Liang-Ting Chen]

Hi,

The discussion remained me that there is a specification of Agda:

https://github.com/agda/agda-spec

It is, however, never complete and has been still for about 3 years ...

Does anyone know if there is any progress or intention of working this?

Cheers,
Liang-Ting

On Wed, 4 Dec 2019 at 13:45, a.j.rouvoet <a.j.rouvoet at gmail.com> wrote:

> Hi Xuanrui,
>
> 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.
>
> Best,
>
> Arjen
> On 12/4/19 10:35 AM, Jesper Cockx wrote:
>
> 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
>>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-- 
— LT
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191204/9d4f4845/attachment.html>