Announcing: MiniRust

The article introduces MiniRust, a project aimed at describing the semantics of a subset of the Rust programming language in a precise and understandable way. The author, Ralf Jung, has been thinking about the semantics of Rust, particularly with regards to unsafe code, and wanted to create a more holistic way to write down his thoughts on the subject.

MiniRust is specified by a reference interpreter written in “pseudo Rust” (now renamed to “specr lang”), which describes the step-by-step process of executing a MiniRust program. The goal is to make the semantics accessible to as many people as possible, while also being precise enough to be useful for tooling and formal verification.

The project is still in its early stages, and there are many features missing, including an aliasing model, unsized types, and concurrency. However, MiniRust can already explain certain aspects of Rust semantics with precision, such as validity invariants, pointer provenance, and casting between pointers and integers.

The author hopes that MiniRust will serve as a starting point for creating an official specification of Rust and encourages others to engage with the project and provide feedback.