Oxide

An implementation of Oxide as described in Oxide: The Essence of Rust.

Background

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.

Terminology

• Safe Rust — the core of Rust, without any unsafe code.
• Language level — a combination of safe Rust and a set of unsafe abstractions that increase the overall expressivity of the language, e.g. Rust1 is safe Rust + Vec<T>.
• Unsafe abstraction — an abstraction that cannot be implemented in safe Rust (absolute) or the current language level (relative) without the use of Rust's unsafe block.
• Lifetime — the span of time from when a value is allocated to when it is deallocated.
• Region — the space on the stack where a value is allocated for its lifetime (see also: why-regions.md).

Navigating this repository

This repository is split into six parts:

1. 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.
2. history/notes/ — an assorted selection of my old notes
3. history/examples/ — a collection of old examples (and counter-examples) at each level
   • Each example is in "proper" Rust syntax for that level and its corresponding oxide form at the time.
4. oxide/ — an implementation of Oxide in OCaml
   • Currently, it's just the type checker, but we will eventually have an interpreter too.
   • We require OCaml 4.08 for user-defined binding form support.
5. reducer/ — a desugarer (simple compiler) from (a subset of) Rust to Oxide
   • Run reducer with RUSTFLAGS='--cfg procmacro2_semver_exempt' for source filename tracking.
6. runner/ — a test harness for driving the reducer/typechecker.
   • This requires the following opam packages: opam install opam shexp stdio yojson utop ppx_deriving

Related Works

• Linear Regions Are All You Need
• L3: A Linear Language with Locations
• A Step-Indexed Model of Substructural State
• Checking Interference with Fractional Permissions ([No Paywall])