~remexre

Minneapolis

https://remexre.xyz

Interests: Programming Languages, Computer Security, Formal Methods, Software Engineering

Trackers

~remexre/stahl

Last active a month ago

~remexre/lemonbot

Last active 6 months ago

~remexre/misc-project-ideas

Last active 8 months ago

~remexre/furing

Last active 10 months ago

#5 mdbook+ninja metabug a month ago

build-system added by ~remexre on ~remexre/stahl

#5 mdbook+ninja metabug a month ago

Ticket created by ~remexre on ~remexre/stahl

mdbook and ninja don't get along too well; noted bugs so far:

  • ninja -t clean fails because we can't enumerate the set of files mdbook generates at configure-time
  • sites don't get rebuilt when mdbook-repl changes

#8 exit code a month ago

Ticket created by ~remexre on ~iptq/garbage

$ garbage put does-not-exist && echo $?
IO error: No such file or directory (os error 2)
0

Should this really be zero?

#6 errors should report relevant file name 5 months ago

Comment by ~remexre on ~iptq/garbage

$ rm tmp out
IO error: No such file or directory (os error 2)

#42 First paragraph of text put above ToC 6 months ago

Comment by ~remexre on ~sircmpwn/man.sr.ht

#4 Literate Stahl 6 months ago

language added by ~remexre on ~remexre/stahl

#4 Literate Stahl 6 months ago

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 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.

#1 Define/document Stahl-the-language 6 months ago

language added by ~remexre on ~remexre/stahl

#2 Port back to rk3399 6 months ago

os added by ~remexre on ~remexre/stahl

#3 Multiprocessing 6 months ago

os added by ~remexre on ~remexre/stahl