Have we looked at the ideas from the Pony language when designing our actor/concurrency story?
https://tutorial.ponylang.io/reference-capabilities/reference-capabilities.html
It looks like in addition to the equivalent of let and var, they have something which can guarantee only a single reference to a particular object (which enforces borrowing), as well as a type of read-only view (the object itself is mutable, but you can wrap it in something which only allows reading to safely send to other threads). They also have an interesting idea of a temporarily mutable object, which can be written to and updated and then frozen.
It is all formally proven to provide lock-free concurrency without data races, etc...