[Agda] Agda 2

[Catarina Coquand]

We will now start the work of defining the next Agda to be implemented 
building
on the current Agda, Agda Light and Mendori.

A first suggestion will be put together by Catarina, Thierry and Makoto 
and will
be sent out for comments by the beginning of September.

We will

1. Define a small core language and a typechecker for it. The aim of 
this typechecker
is not to give good error messages or do any interactions with users, 
nor being efficient. Instead
it should be a small program in which we can trust, and the aim should 
be to
prove the code correct. The semantics of the core language should also 
be described this time :-) .

2. Define a bigger (but not big) language which is defined in terms of 
the core.
The interactive system, with its own typechecker, will be implementing 
the bigger language.

One might wonder why having two typecheckers and not translate directly 
to the core language, but
it is difficult to give good error messages and pretty printing when 
everything is translated into
a core language. Users might not recognize at all what is printed.


At a meeting in Japan last week we discussed the following points

*Agda2 goals 
** even full sys must be a small system.
** clear semantics
** must be usable as a programming language
proliferate - general recursion syntax?
   (non-termination allowed)
 - in-built types and constants (sp. arithmetic)
 - in full sys., overloading with implicit args
 - I/O, connections with OS.
   in connection with the plugin interface (Ulf's
   mechanism?)
 - syntax that can be handled by GF / BNF converter. (how'bout user-defined precedence?)
** Human readable proofs
   - flexibility in how much detail can be presented.
   - structuring (packages etc.)
** To be fixed and working early, so that
   no more provisional prototypes are to prol.
   Else, there need to be a lot of work adopting
   plugins again etc.
*Transition from Agda to Agda2
   aims for the end of 2005...
 - soft transition. Agda should be translatable to
   Agda2 core.
 - Agreed: try to keep what Agda already have.
 - (may make small changes for uniformity
    e.g. layout-rules. (cf. Aarne's comment from last AIM))

Do you who were not in Japan some more words of wisdom (besides the one 
you have allready sent us?)

We are also interesteding comments about a good process to use (yes, I 
know, it is Software Engineering) but
how does one, by a good process(?), avoid that Agda again becomes a 
one-developer system? Have
developers that knows the code of one another? That only well-written 
and documented code is added to the
system?


  Catarina