Note about specification language
I don't know if this is a long-time project, but I'd like to share an idea.
Some time ago I stumbled upon Lem [1]. Some PL group used it to write their specifications for a program that is then translated into Isabelle or Coq. Currently, there is not translation into Agda, however, I think, that using a specification-like language as Lem is the way to go instead of implementing an translation two times.
I see two potential projects here.
(1) Implement a translation from Lem to Agda (2) Implement the translation for Lem