Seems like this is a step in that direction.
It’s neat what falls out of type theory. Counting Immutable Beans was another eye-opening paper worth reading if you’re curious like me.
Uniqueness types (which Rust can only be said to have as an implementation detail of the borrow checker’s running, as opposed to having programmer assignable uniqueness qualifier syntax for construction of types) are semantic constructs that a user places on types which then restrict the operations available for that object. In this paper and in Koka, the language that semi-inspired the exploration here, the functional-in-place mutation scheme is an optimization performed by the compiler in those cases where the resulting code is probably equivalent to the surface level syntax. Said surface level syntax presenting a logical view of the program as only have persistent, immutable objects.
The implicit novelty, although this paper is more an exploration of existing concepts in a specific environment (i.e. no GC at run time), is that there is no annotation burden or conceptual distinction to be made by users of the language to receive the performance benefits of mutation where available.