[Agda] Future of Agda?

[Pierre Hyvernat]

Hello (again)...


It is nice to see all the work being done in Agda at the moment, but I
have some general questions concerning the "goals" we want to achieve
with Agda.


Right now, it seems that the idea is to continue hacking the old Agda
code to implement the last nice ideas people have had. (Implicit
arguments, classes, pluggins etc.)


I gathered from the first Agda meeting in October that ideally, the
current code will be replaced by a new version in the future.
("Agda2", see also the "Agda-light" implementation work by Ulf and
Andreas...)



I know it is not the right time to decide things, but I think we should
start thinking about what we want to achieve.

There are two main trends:

  * getting a bigger, better Agda (with all the possible technology one
    can think of)

  * getting a smaller, better Agda (with a source code as simple as we
    can get it)


My opinion is that we should be aiming for the second. I don't think we
can compete with existing proof-assistants; and I would rather see Agda
as some kind of "playground" for testing new ideas.

Another good use is education. Both Erik Palmgren and Anton Setzer have
used Agda in courses; and it went quite well. (I actually learned Agda
from Erik's course!)
I am afraid that getting something too big will make that kind of use
difficult...



My view is thus that we should have a "core Agda" as small and nice as
possible. This would contain more or less what Agda contains now.  (I
guess this is what Agda-light is aiming at.)

Together with that, we should try to design a good pluggin mechanism and
an emacs interface (pretty much similar to what we use now) and good
documentation.

This would be similar to the "Haskell 98" part of Haskell, though not as
rigid.


To this, we add "packages", pluggins, libraries or whatever so that
people who want to can use it for more specific tasks.


Ideally, it should be possible for "anybody" to understand the structure
of the core-code to start playing with it. (Adding strange typing rules
etc.)




Let the discussion begin...




Pierre Hyvernat
--