A data race that doesn't compile (in Rust)
The article introduces Ruxe, a Rust library that uses type-level disjointness to enforce at compile time that no two mutably borrowed data can alias, preventing data races. By encoding unique ownership and disjointness constraints into the type system, Ruxe ensures that programs violating these constraints fail to compile, offering a static guarantee against data races without runtime overhead.
Background
Rust is a systems programming language famous for its "borrow checker," which enforces memory safety at compile time (no null pointer dereferences, no use-after-free) without needing a garbage collector. Its type system has been steadily extended with features like const generics (compile-time constants as type parameters) and GATs (generic associated types), bringing more runtime checks into the compiler.
This post digs into a subtle, cutting-edge corner of Rust's type system: using type-level disjointness proofs (i.e., proving at compile time that two regions of memory cannot alias) to statically prevent data races. The author proposes a library called "ruxe" that encodes these proofs so that a program that would race at runtime instead fails to compile — catching the bug before it ever runs.