Proof General is based around a core system of script management for proof scripts. But the idea of script management is not restricted to proof assistants, it makes sense for many interactive scripting languages. It deserves to be better known and used. A worthwhile project would be to rewrite the core script management features of Proof General so that they could work for arbitrary interactive scripting languages, and instantiate to Proof General as well as languages such as ML, Haskell, LISP, Scheme, Python, and even Emacs Lisp itself.
An alternative version of this project is to implement a generic basis for script management which does not depend on Emacs, but uses a similar protocol to communicate with other text editors or display widgets. This could be implemented in SML, OCaml, Java, C++, or any other suitable language.
Skills: Proficient Emacs Lisp (or other programming language), knowledge of scripting languages desirable.
Proposer: David Aspinall.