MiniRust: A Core Language for Specifying Rust
summary
Two demos show concrete, reproducible failures: reading an uninitialized i8 decodes to an error and the interpreter flags undefined behavior at decode time, and pointer arithmetic that produces equal addresses but different provenance lets optimizations observe stale values. MiniRust implements an executable operational spec as a MiniRust interpreter written in Rust‑like code (Specker), models memory as untyped bytes with provenance-annotated bytes, provides encode/decode for high‑level values, covers most core features (SC concurrency only), and is on GitHub with student-contributed extensions.
AI-written summary · about
chapters (12)
- 0:00Welcome to MiniRust
- 1:47Undefined behavior in unsafe Rust
- 3:57Specifying unsafe Rust challenges
- 5:18MiniRust design goals
- 6:23MiniRust core language
- 9:12Memory and pointer analysis
- 13:25Uninitialized memory and integers
- 15:51Pointer provenance implications
- 19:18Provenance in MiniRust interpreter
- 20:02MiniRust pipeline and interpreter
- 21:25MiniRust features and plans
- 22:30Q&A: weak memory and provenance
