Future Of Agda

Ulf: Future of Agda

Ulf's job running out at the end of year. Grant app result on November.

Few other ppl know and can work e.g. Nisse, Andreas, Makoto, ...

Thorsten: Maybe a good time to reimplement Agda.

Ulf: Manpower problem

Th: Only Ulf knowing the detail is more expensive in medium term...

JP: The code is not that bad.

Andreas: re-implementation always promising just getting back where we were in 2years Bengt: Not true. We do have a better agda. Don't be too pesimistic. (re Ulf too)

Conor: On a positive note. Agda at a cross road.

  Decide to fail, or, try to be successful in the already existing comm with Agda-habit.   Compilation!

Th: We should take advantage of having ppl who know Haskell and Agda.

    Difficult to get funding for maintaining software.  Need to pretend
    a blue-sky research

Bengt: It _is_ a blue-sky research, just different from writing papers.

  Matter of how to describe.

Andreass: There are a lot of publishable issues re Agda implementation. JP: (Chalmers situation.) Peter's new student., Nisse,. Nisse: Strathclyde activities? Conor: No piece of code lasts more than 6 mo.(in Epigram 2)

Th: This is more like a funeral...

JP: More open process for development, Public review of patches, etc. Bengt: There' danger about it.. JP: The goal is more ppl start reading rather than writing just now.

Nisse: IRC shows some ppl tried and gave up, don't know why

Andreas: For Twelf, Frank Pfenning is writing all the pre/post conditions etc. for each function.

  Novice developer needs such security

Th: Last AIM's 'quoteGoal' was done by Ulf showing how to Th, and that was a non-trivial process. Needs those things are documented.

JP: We should be insisting on commenting code, recording Ulf's wisdom.

Conor: I suggest Complete ban on Ulf implementing Agda! New features should be implemented by somebody else; then more ppl start learning the code.


Conor: Recollection of AIM1... Catarina giving several lectures and then a lot of ppl working on the internal... Maybe that style could be revived...

Ulf: Summarising

Th: About indoctrinating Phd students. Ulf saw Agda1, was too complicated, started writing Agda-Light, ...

... More and more ppl worldwide are using Agda... It would be a scandal if Ulf doesn't get a job at Chalmers after this sort of success.

Try to encourage students to become a heroe of Type Theory like Ulf.

Conor: ICFP this year has noticeable Agda presence.

Andreas: Over three hundred issues in tracker.

Ulf: Important thing is to get more ppl involved

JP: Documenting and Commenting. Public patch submission/review.

Nisse: Agda-mailing list can be used.

Conor: Attraction more valuable than revulsion. If it becomes necessary(too much dev traffic/chatting), fork off a new mailing list.

XX, U-Penn, Iowa ppl could study the Agda code before re-implementing.

JP: Can I send the patch to Agda-mailing list? Nisse: Sure.

Conor: The right kind of traffic on Agda list would XXX



  • Nisse could be the chief maintainer of Agda (in case Ulf's gone)
  • Hope to recruite more ppl get involved and inpart more knowledge about the code published.
  • Make the dev process more public. Use Agda-mailing list for this purpose too. If a problem occurs, fork-off.


  • Overview of the code structure on the Wiki 'How to add X' etc.


  • Ulf giving a public lecture on 'How to XXX Agda". Next AIM.

Conor: it has to be combined with a sprint, otherwise ppl just forget.