Emacs already provides powerful outline facilities (cf. the outl-minor-mode setup for the well-known auc-tex package). Similarly, proof systems such as Isabelle/Isar are inherently based on block-structured proof texts, with compositional proof checking.
But Proof General currently offers a mostly linear model of incremental script management. The aim of this project is to extend that model to a hierarchic one: e.g. sub-proofs could be suppressed in the presentation, or even temporarily suspended (to achieve top-down development).
Outline support would be useful for the large scale structure of formal developments as well, e.g. support the basic arrangement into logical section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX).
Skills: Some understanding of the workings of Emacs outline mode and Proof General script management. Good portion of Emacs lisp knowledge.
Proposer: Markus Wenzel.