A precise specification for "Rust lite / MIR plus"
If you prefer video to text, I recently presented MiniRust at RustWeek 2025. Furthermore, you can check out this older, but more in-depth presentation of MiniRust for the RFMIG.
MiniRust is the cornerstone of my vision for a normative specification of Rust semantics. It is an idealized MIR-like language with the purpose of serving as a "core language" of Rust. This is part of a larger story whose goal is to precisely specify the operational behavior of Rust, i.e., the possible behaviors that a Rust program might have when being executed: the behavior of a Rust program is defined by first translating it to MiniRust (which is outside the scope of this repository), and then considering the possible behaviors of the MiniRust program as specified in this document. That translation does a lot of work; for example, traits and pattern matching are basically gone on the level of MiniRust. On the other hand, MiniRust is concerned a lot with details such as the exact evaluation order, data representations, and precisely what is and is not Undefined Behavior.
To separate the complexities of memory from the semantics of MiniRust statements and expressions, we introduce the MiniRust memory interface:
think of memory as implementing some trait; MiniRust semantics is generic over the actual implementation of that trait.
The interface between the MiniRust language (specified in lang) and its memory model (specified in mem) is untyped and byte-oriented (but "bytes" are a bit more complex than you might expect).
For now, we only define the memory interface, but do not give an implementation.
Even without deciding what exactly the final memory model will look like, we can answer a surprising amount of interesting questions about Rust semantics!
On the MiniRust language side, the most important concept to understand is that of a value and how it relates to types. Values form a high-level, structural view of data (e.g. mathematical integers); types serve to relate values with their low-level byte-oriented representation. Types are essentially just parameters attached to certain operations to define the (de)serialization format. Well-formedness of a MiniRust program ensures that expressions and statements satisfy some basic typing discipline, but MiniRust is by design not type-safe.
The most precise way to write down the MiniRust spec would be with mathematical notation.
However, without LaTeX this is a pain, and it also involves a lot of jargon which hurts accessibility of the spec.
That's why the MiniRust spec is written as an interpreter, so the spec itself is code.
That begs the question, which language do we write that code in?
We are using a kind of "Rust-like pseudo-code" called specr lang:
imagine Rust without all the restrictions about sizedness and pointer indirections for recursive types (we could implicitly insert Arc where needed).
We use generic type names like List, Map, Set rather than concrete implementations like Vec, HashMap, HashSet, since the implementation details do not matter.
We also assume some "obvious" language extensions -- basically, it should always be clear what is meant to anyone with some Rust experience, even if this is not actually legal Rust.
All types except for mutable references are Copy (let's just imagine we implicitly Clone where needed), and we use fn(T) -> U notation even for closures that can capture arbitrarily.
We use panic! (and unwrap and slice indexing and similar standard Rust operations) to indicate conditions that should always hold; if execution ever panics, that is a bug in the specification.
Our functions are generally pure; they can write to mutable references, but we can consider this to be implemented via explicit state passing. When we do need other effects, we make them explicit in the return type. The next sections describe the effects used in the MiniRust interpreter.
We use Result to make operations fallible (where failure indicates UB or machine termination).
We use a throw_ub! macro to make the current function return a UB error value, and throw_machine_stop! to indicate that and how the machine has stopped.
Similarly, we use throw!() inside Option-returning functions to return None.
In order to wrap a value t: T as Result, Option or NdResult (see next subchapter), we use the function ret(t).
See the prelude for details.
We also need one language feature that Rust does not have direct support for: non-determinism.
The return type Nondet indicates that this function picks the returned T (and also its effect on &mut it has access to) non-deterministically
This is only used in the memory model; the expression language is perfectly deterministic (but of course it has to propagate the memory model's non-determinism).
In a function returning Nondet, we use ? for monadic bind (this is more general than its usual role for short-circuiting), and the return value is implicitly wrapped in monadic return.
The function pick(impl Distribution, fn(T) -> bool) -> Nondet will return a value of type T such that the given closure returns true for this value.
This non-determinism is interpreted daemonically, which means that the program has to be correct for every possible choice.
In particular, if the closure is |_| false or T is uninhabited, then this corresponds to "no behavior" (which is basically the perfect opposite of Undefined Behavior, and also very confusing).
For the purpose of making the spec executable, pick also receives a Distribution argument.
This argument does not affect the set of possible program behaviors, it is purely a hint for the interpreter to sample suitable candidates.
Similar to pick, the function predict(fn(T) -> bool) -> Nondet also returns a T satisfying the closure, but this non-determinism is interpreted angelically, which means there has to exist a possible choice that makes the program behave as intended.
In particular, if the closure is |_| false or T is uninhabited, then this operation is exactly the same as hint::unreachable_unchecked(): no possible choice exists, and hence ever reaching this operation is Undefined Behavior.
The combined monad Nondet> is abbreviated NdResult, and in such a function ? can also be used on computations that only need one of the monads, applying suitable lifting:
Result -> NdResult is trivial (just use monadic return of Nondet); Nondet -> NdResult simply maps Ok over the inner computation.
So just to be clear, there are two Rust dialects at play here:
specr-transpile can translate specr lang into Rust, so that we can run and test the MiniRust interpreter.
In the future, we'll hopefully have tools that can translate specr lang into the formal language of a theorem prover like Coq, so that we can establish formal proofs about the MiniRust specification.MiniRust is extremely incomplete! Some features are entirely missing (e.g. floats). There are lots of TODOs. The language syntax is also missing many of the Rust operators and casts. I hope to slowly chip away at all this over time. If you want to help, please talk to me -- PRs to add missing features are very welcome. :) But we also need to ensure the entire document stays coherent, and I already have vague ideas for many of these things.
v: Value, val: Value, value: Value?
What do we use for ValueExpr? Similar questions exist around Place/PlaceExpr and ty: Type/type: Type.You might wonder how this project compares to Niko's a-mir-formality. The obvious answer is that Niko is much better at picking names. ;)
On a more serious note, these projects have very a different scope: MiniRust is only about the operational semantics. a-mir-formality is a lot more ambitious; as the inaugural blog post explains, it aims to also formalize traits, type checking, and borrow checking -- all of which I consider out-of-scope for MiniRust. a-mir-formality is machine-readable and written in PLT redex; MiniRust uses pseudo-code that is not currently machine-readable (but I have ideas :). The primary goals of MiniRust are to be precise and human-readable; I would argue that while PLT redex is more precise than the style I use, it does lack in readability when compared with Rust-style pseudo-code. I am willing to sacrifice some precision for the significant gain in readability, in particular since I think we can recover this precision with some amount of work. And finally, the "operational semantics" layer in a-mir-formality is "not even sketched out yet", so as of now, the projects are actually disjoint
No open issues yet, or sync has not completed.