Isn't this solved perfectly with an affine or linear type-aware optimizing compiler? Where all data is immutable unless the types prove to the compiler that there are no mutation conflicts. I believe Rust implements this and Idris 2 does so as well with quantitative type theory.