Summary
The goal is to build a specification for the whole of Rust,
from surface syntax down to detailed semantics,
that is both legible and executable.
As design axioms, we want this specification to be:
- Understandable by non-experts, serving as a reference that users can reach for;
- Executable, so we can test it and ensure correctness;
- Easy to evolve, so it can be at the heart of language evolution;
- Well-structured, so it can be turned into maths and be amenable to formal analyses.
We propose that this specification would be a program written in a Rust-flavored literate language
(probably [specr]), interspersed with English explanations.
As a program, it would be an interpreter capable of executing real Rust source files.
As a specification, it would describe the meaning of the programs supported.
The plan is to build on top of the existing executable specification efforts,
namely [a-mir-formality] and [MiniRust],
by bridging the gap between surface Rust syntax
and these semantic models.
We propose to bridge that gap by successively desugaring
expressive syntactic constructs down to more basic ones,
as sketched in [rust-via-desugarings].
This will be a multi-year effort.
For this goal period the focus will be
on putting the bases in place,
namely parsing, integration with a-mir-formality/MiniRust,
tests, and fully fleshing out a couple features.
Tasks and status
Note: we have updated the body to match the 2026 goal. Your original text is preserved below.
Details
Summary
The goal is to build a specification for the whole of Rust,
from surface syntax down to detailed semantics,
that is both legible and executable.
As design axioms, we want this specification to be:
- Understandable by non-experts, serving as a reference that users can reach for;
- Executable, so we can test it and ensure correctness;
- Easy to evolve, so it can be at the heart of language evolution;
- Well-structured, so it can be turned into maths and be amenable to formal analyses.
We propose that this specification would be a program written in a Rust-flavored literate language
(probably [specr]), interspersed with English explanations.
As a program, it would be an interpreter capable of executing real Rust source files.
As a specification, it would describe the meaning of the programs supported.
The plan is to build on top of the existing executable specification efforts,
namely [a-mir-formality] and [MiniRust],
by bridging the gap between surface Rust syntax
and these semantic models.
We propose to bridge that gap by successively desugaring
expressive syntactic constructs down to more basic ones,
as sketched in [rust-via-desugarings].
This will be a multi-year effort.
For this goal period the focus will be
on putting the bases in place,
namely parsing, integration with a-mir-formality/MiniRust,
tests, and fully fleshing out a couple features.
Tasks and status
Summary
The goal is to build a specification for the whole of Rust,
from surface syntax down to detailed semantics,
that is both legible and executable.
As design axioms, we want this specification to be:
We propose that this specification would be a program written in a Rust-flavored literate language
(probably [specr]), interspersed with English explanations.
As a program, it would be an interpreter capable of executing real Rust source files.
As a specification, it would describe the meaning of the programs supported.
The plan is to build on top of the existing executable specification efforts,
namely [a-mir-formality] and [MiniRust],
by bridging the gap between surface Rust syntax
and these semantic models.
We propose to bridge that gap by successively desugaring
expressive syntactic constructs down to more basic ones,
as sketched in [rust-via-desugarings].
This will be a multi-year effort.
For this goal period the focus will be
on putting the bases in place,
namely parsing, integration with a-mir-formality/MiniRust,
tests, and fully fleshing out a couple features.
Tasks and status
Note: we have updated the body to match the 2026 goal. Your original text is preserved below.
Details
Summary
The goal is to build a specification for the whole of Rust,
from surface syntax down to detailed semantics,
that is both legible and executable.
As design axioms, we want this specification to be:
We propose that this specification would be a program written in a Rust-flavored literate language
(probably [specr]), interspersed with English explanations.
As a program, it would be an interpreter capable of executing real Rust source files.
As a specification, it would describe the meaning of the programs supported.
The plan is to build on top of the existing executable specification efforts,
namely [a-mir-formality] and [MiniRust],
by bridging the gap between surface Rust syntax
and these semantic models.
We propose to bridge that gap by successively desugaring
expressive syntactic constructs down to more basic ones,
as sketched in [rust-via-desugarings].
This will be a multi-year effort.
For this goal period the focus will be
on putting the bases in place,
namely parsing, integration with a-mir-formality/MiniRust,
tests, and fully fleshing out a couple features.
Tasks and status