[Agda] Agda 2

[Peter G. Hancock]

    > on the current Agda, Agda Light and Mendori.

What's 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.

    >  - I/O, connections with OS.
    >    in connection with the plugin interface (Ulf's
    >    mechanism?)

What is this?  

I'm fairly pessimistic about any concrete proposals for IO emerging
from what Pierre and I have been doing.  It might cheer me up to read
a viable idea (in a few sentences or a paragraph) for IO in
dependently typed programming.

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

I recommend you continue the Chalmers condition of having 
witty names for your systems. I thought Another God-Damned
Acronym was superb.  Also alf->half. 

Seriously, I think it sounds great that there is so much
agreement that Agda÷2 should be something in its basis simple 
to implement and understand, and solid. 

    > 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?

Why not think about an "open" model, in which anyone who is interested
can read a blog of what is going on, the latest code, maybe make
comments etc?

There is nothing to improve the quality of one's code to know
that people who are sufficiently obsessed may be reading it. 

This is something like what Conor et al are doing in Nottingham.

Peter