The essence of Rust.
An implementation of Oxide as described in Oxide: The Essence of Rust.
To get a sense of the terminology and why the semantics is structured how it is (i.e. into levels), I highly recommend reading Niko's post about observational equivalence in Rust. This should at least be sufficient to understand why we're talking about levels of Rust, but it may well provide other useful insights as well. Niko's recent work on non-lexical lifetimes features some key similarities to our approach, and may aid in its understanding.
Vec<T>
.unsafe
block.why-regions.md
).This repository is split into six parts:
history/
— largely-iterative prior attempts at building & designing Oxide
ownershipv1
and ownershipv2
both have
some notes included that might be insightful to some degree. Evidently, I got lazy afterward
and stopped writing actual prose in the models. Afterward, I switched to LaTeX.history/notes/
— an assorted selection of my old noteshistory/examples/
— a collection of old examples (and counter-examples) at each level
oxide
form at the time.oxide/
— an implementation of Oxide in OCaml
reducer/
— a desugarer (simple compiler) from (a subset of) Rust to Oxide
RUSTFLAGS='--cfg procmacro2_semver_exempt'
for source filename tracking.runner/
— a test harness for driving the reducer/typechecker.
opam install opam shexp stdio yojson utop ppx_deriving