This is one small piece of the work that's going to need doing to get Rust properly described.
It's not "useful" in the sense of being something that you'd actually run.
This is a start on the lowest layer of the description, describing the "abstract machine" that runs Rust programs; it assumes that all borrow-checking and type-checking has already been done, generics have been expanded, and so on.
The other two big pieces that will need doing are properly describing the type system, and properly describing how the high-level features that aren't strictly necessary can be "lowered" into simpler forms.
> It's not "useful" in the sense of being something that you'd actually run.
What if we could actually run it (stay with me for a second) with a well known interpreter such as python3 or v8?
That is the direction py2many has taken. Trying to define a small subset of python + missing rust features (pattern matching as an expression), interfacing with formal verification methods such as z3 and then finally building a transpiler to transpile this language to rust.
My goal is that we can actually run it, but that would still only be useful for the following things:
- Testing the spec itself
- Ensuring that a more production-grade interpreter like Miri has the same semantics as the spec it claims to implement
It's not intended that unsafe Rust authors would ever run the MiniRust interpreter; if they want something like that, they should run Miri instead. They might still read the MiniRust interpreter sources to figure out what the heck Miri is doing.
It's not "useful" in the sense of being something that you'd actually run.
This is a start on the lowest layer of the description, describing the "abstract machine" that runs Rust programs; it assumes that all borrow-checking and type-checking has already been done, generics have been expanded, and so on.
The other two big pieces that will need doing are properly describing the type system, and properly describing how the high-level features that aren't strictly necessary can be "lowered" into simpler forms.
In the last year there's been some real work on the first of those under the name "A MIR Formality": https://nikomatsakis.github.io/a-mir-formality/docs/intro
Maybe the existing Rust Reference will turn into the second.