Emacs has a mechanism for customizing the editing behaviour of buffers based on their major mode. A buffer can only have one major mode, but in literate styles of programming and proving we want to mix program text with documentation in a single file. A way of multiplexing major modes is needed, so that different regions of a buffer can be edited in different modes. One approach may be to use "views" onto untangled buffers, although it isn't clear how search and replace, etc, should behave in this case.
Emacs hackers may already have worked on this problem and solved it sufficiently well (does anybody know?), in which case this project might degenerate into applying the work for Coq and Isabelle/Isar, as a feasibility demonstration.
Skills: A passion for Emacs and Emacs Lisp.
Proposer: David Aspinall.