> ...there is an entire field of pointer analysis and escape analysis that can and does infer uniqueness and reasons about whether two references can be aliases.
You can't do this automagically in the general case, you really do need something much like separation logic. (And of course the Rust borrow checking semantics can be seen as a simplified variety of separation logic.)
Classes and fields don't give you completely local reasoning about mutable state, because class/object A can end up depending on the mutable state of class/object B. And class inheritance as found in Java adds all sorts of further complexity of its own, especially as programs evolve over time.
You can't do this automagically in the general case, you really do need something much like separation logic. (And of course the Rust borrow checking semantics can be seen as a simplified variety of separation logic.)
Classes and fields don't give you completely local reasoning about mutable state, because class/object A can end up depending on the mutable state of class/object B. And class inheritance as found in Java adds all sorts of further complexity of its own, especially as programs evolve over time.