A recent paper by the author: "A Flexible Type System for Fearless Concurrency" pdf[1]. In which is discussed a technique for creating memory regions that a compiler can use for proving there are no race condition; with less ceremony than in Rust.
[1] https://www.cs.cornell.edu/andru/papers/gallifrey-types/fear...