MiniRust: A core language for specifying Rust
summary
MiniRust is a precise, operational core language plus an executable interpreter (Specker) that lowers Rust and answers whether a program has UB by running the spec. Memory models allocations as lists of initialized/uninitialized bytes, values are encoded/decoded to bytes and encode/decode returning None signals invalid representation ⇒ UB. It models provenance and tree‑borrows, uses a nondeterministic pick for choices, already runs many Rust features, and the demo concretely flags the earlier surprising UB.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:08Integer assertion failure
- 6:43Rust and C specs challenges
- 8:05Desired Rust spec properties
- 10:12MiniRust core language
- 12:38MiniRust syntax and semantics
- 16:07Operational semantics design
- 17:50MiniRust memory model
- 19:55Types and values in memory
- 21:40Uninitialized bytes decoding
- 23:48Demo: interpreter detects UB
- 24:49Translating Rust to MiniRust
- 25:31Bool and invalid representations
- 26:55Padding in type representations
- 28:41MiniRust status and contributors
- 29:24Future of MiniRust spec
- 30:08Q&A: threads and nondeterminism
- 32:55Q&A: provenance and aliasing
