Interests: Programming Languages, Computer Security, Formal Methods, Software Engineering
mdbook and ninja don't get along too well; noted bugs so far:
ninja -t cleanfails because we can't enumerate the set of files mdbook generates at configure-time
- sites don't get rebuilt when
$ garbage put does-not-exist && echo $? IO error: No such file or directory (os error 2) 0
Should this really be zero?
$ rm tmp out IO error: No such file or directory (os error 2)
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
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.