a-mir-formality VS miniPerl

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

Using "mini" to mean a subset of the language rather than a version for small systems has precedent. For example in the Perl community, miniperl is a subset of Perl. It's mostly used to bootstrap builds of the full language, but in theory can be used separately as a restricted programming language. It's also the name of a module, ExtUtils::Miniperl, for Perl (https://metacpan.org/pod/ExtUtils::Miniperl) that builds miniperlmain.c and perlmain.c files to bootstrap the compilation of the language system. This is not to be confused with the Raku project on Github called "miniPerl" (https://github.com/grondilu/miniPerl) which compiles subsets of Perl via the Lambda calculus to JavaScript output.

I'd personally pretty much always expect "mini" or "r" (as in "rperl", a restricted subset of Perl with C++ connections) versions of a language to be restricted subsets for some purpose (rperl's is to give away flexibility for performance while maintaining a good portion of the original language).

I've seen an "e" or "emb" prefix or a "small", "tiny", "micro" or "µ" (or "u") prefix to mean a small toolchain version several places, like SmallC or uclibc or Mikroe's mikroC. It wouldn't surprise me to see a "nano" version of a language tool either. Sometimes these are subsets as well, but to fit the size constraints of the target rather than for constraining the input for its own sake.