Minneapolis
Interests: Programming Languages, Computer Security, Formal Methods, Software Engineering
Ticket created by ~remexre on ~remexre/stahl
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
mdbook-replchanges
Ticket created by ~remexre on ~iptq/garbage
$ garbage put does-not-exist && echo $? IO error: No such file or directory (os error 2) 0Should this really be zero?
Comment by ~remexre on ~iptq/garbage
$ rm tmp out IO error: No such file or directory (os error 2)
Ticket created by ~remexre on ~remexre/stahl
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
TermandValuetypes interm.rsandvalue.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 ineval.rs, adding a type inference rule intyck.rs, and adding a parsing rule inelab.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.