This doesnt seems to be meaningfully different from Rust.

> does not require tracing garbage collection

Just call it garbage collection.

(Applies in two ways: if you think that garbage collection subsumes reference counting then this language doesn’t require garbage collection in the sense that it also doesn’t require reference counting; if you think that garbage collection does not subsume reference counting then there’s no point in saying three words when you can say two.)

It's less specified than rust. For example, you can bind references to individual collection elements here. It doesn't seem to prohibit borrowing a dynamically indexed element either, which is one hell of a static analysis lift. Seems like you can also have simultaneous references to distinct static indices (e.g. &mut arr[0] and &mut arr[1]) as long as you don't do invalidating operations, which isn't expressible in NLL or polonius. That's feasible for a borrowchecker at least.