Specifically, we consider the "spine" of a linked list to be its own private "region", separate from the elements' region. This lets us freeze the spine region, while keeping the elements region mutable.
This mechanism is particularly promising because it likely means one can iterate over a collection with zero run-time overhead, without the normal restrictions of a more traditional Rust/Cyclone-like borrow checker. We'll know about this iterating benefit for sure when we finish part 3 (one-way isolation [1]); part 1 landed in the experimental branch only a couple weeks ago [2].
The main difference between the two approaches is that Vale doesn't assume that all elements are self-isolated fields, it allows references between elements and even references to the outside world. However, this does mean that Vale sometimes needs "region annotations", whereas the paper's system doesn't need any annotations at all, and that's a real benefit of their method.
Other languages are experimenting with regions too, such as Forty2 [3] and Verona [4] though they're leaning more towards a garbage-collection-based approach, where Vale is more like a memory-safe C++.
Pretty exciting time for languages!
[0] https://verdagon.dev/blog/zero-cost-borrowing-regions-overvi...
[1] https://verdagon.dev/blog/zero-cost-borrowing-regions-part-3...