It'd be quite neat to have a proper literate programming tool for Stahl source code, especially if it would allow the self-hosting implementation's source to be re-used as language documentation. In particular, a major annoyance with reading the current Rust implementation is the degree to which the implementation of a term is spread throughout the code.

To add a new type former requires modifying the definition of the Term and Value types in term.rs and value.rs, adding a few methods to match (some of which could plausibly be generated by a derive macro, others cannot), adding a (trivial) reduction rule in eval.rs, adding a type inference rule in tyck.rs, and adding a parsing rule in elab.rs. Once the reader gets the hang of how these functions all piece together, most of the details of each method are somewhat irrelevant; rather, the useful thing is to be able to see how a term is implemented throughout the language implementation.

WEB-style literate programming is probably the most well-explored idea in this space, but something based on Leslie Lamport's How to Write a Proof is worth exploring too. Especially for systems that can be specified formally, being able to "expand" a high-level prose+code explanation into one that's progressively more complete code seems very useful.