Ah - the author does call out that Rust can’t do local reasoning perfectly. The other place it comes up aside from the Sync example I describe is RefCell which similarly lets you mutate from behind a shared reference thus also violating local reasoning. The author also describes why Rust deviated here (the niche Rust was moving into with systems programming often needs an escape hatch for some small amount of non-local mutability)