a-mir-formality VS theory-exploration-benchmarks

Racket is very used in the PLT community (programming language theory) for prototyping programming languages. Lots of cool stuff in this area.

For example, the MIR formality [0] project of the Rust programming language to formalize MIR (their intermediate language) was first prototyped in Racket [1], then rewritten in Rust. [1]'s readme give a rationale:

> For the time being, the model is implemented in PLT Redex. PLT Redex was chosen because it is ridiculously accessible and fun to use. It lets you write down type system rules and operational semantics and then execute them, using a notation that is very similar to what is commonly used in published papers. You can also write collections of unit tests and fuzz your model by generating test programs automatically.

> The hope is that PLT Redex will prove to be a sufficiently accessible tool that many Rust contributors will be able to understand, play with, and extend the model.

> One downside of PLT Redex is that it doesn't scale naturally to performing proofs. We may choose to port the model to another system at some point, or maintain multiple variants.

[0] https://github.com/rust-lang/a-mir-formality

[1] https://github.com/rust-lang/a-mir-formality/tree/1f40120f09...

But MIR optimizations are a bit of a mess right now. The semantics of MIR are not completely settled but that is an area of active work: https://github.com/nikomatsakis/a-mir-formality

That's happening separately, in the "mir-formality" project: https://github.com/nikomatsakis/a-mir-formality

The two projects are related, but have different objectives (mir-formality includes traits and borrow checking, while MiniRust focuses on operational semantics).

I chose Racket for a project that involved lots of AST manipulation. Those ASTs were already in s-expression format, so Scheme seemed a natural fit.

The lack of static types was annoying; Typed Racket helped, but was so slow I only enabled it during unit tests (more precisely: Typed Racket functions can be faster than those written in normal Racket, but calling them from normal Racket functions will be slow as it performs run-time checks)

https://github.com/Warbo/theory-exploration-benchmarks/tree/...

> "CLI args are usually passed around explicitly" -- I think this is a pro, not a con.

Sure; I never said it's a con. They have different characteristics, and are both useful in certain situations :)

> I think the correct term for "things the caller knows better than the implementor" are parameters.

True; that's also the name Racket gives to dynamically-scoped variables https://docs.racket-lang.org/guide/parameterize.html

In fact, Racket uses a parameter (dynamically-scoped variable) to store the environment. This is actually slightly annoying, since the parameter is one big hashmap of all the env vars; but I usually want to override them individually. One of my Racket projects actually defines a helper function to override individual env vars makes a copies all the other environment ( made a are contained in a parameterhttps://github.com/Warbo/theory-exploration-benchmarks/blob/...