Allocations live in their own plane, the root allocated typed being the root node of that plane. For threads, I’m still working on that, don’t have a super cool answer yet
Another thing - when a value is moved or dropped the plane’s type changes from T to shape(T). shape(T) contains unspecified data but has the size and alignment of a T. So you couldn’t safely prove that a moved out/dropped shape(T) is a T
This only works if you make every allocation its own plane, and scope all borrows to the lifetime of the plane, with a move terminating all borrows, at which point this is equivalent to rust, just with confusing jargon.
Correct, every allocation is its own plane. The nice thing about this model is that you don't need to explicitly call out lifetimes. I also believe that lifetimes aren't really a good model of what actually happens in memory. This model is more powerful because it understands relationships between planes in memory, which Rust's model doesn't. This is why it requires mutable borrows to be unique which is oftentimes overly restrictive. For instance this is not valid Rust:
let x = vec![1, 2, 3];
let a = &mut x[0];
let b = &mut x[1];
swap(a, b);
Because Rust doesn't really know the difference between the whole Vec an element within the vec. Therefore it treats any mutation as one that could potentially invalidate anything with the same lifetime and doesn't compile. So I believe the plane model to be strictly better because it allows for this and still prevents the real scary thing:
let x = vec![1, 2];
let a = &mut x[0];
x.push(3);
a = a + 1;
I’m not quite sure I understand your question. But if x is a vector of things that contain allocations, the compiler will track a plane for them and represent them sparsely as needed be.
The compiler tracks all of the currently living planes. The compiler tracks from which plane each borrow is borrowed. Once the plane it is borrowed from dies that borrow is no longer valid
[–] jordan_bonecut 3 days ago
[–] 0c3ca83 3 days ago
[–] jordan_bonecut 3 days ago
[–] 0c3ca83 3 days ago
[–] jordan_bonecut 3 days ago
let x = vec![1, 2, 3]; let a = &mut x[0]; let b = &mut x[1]; swap(a, b);
Because Rust doesn't really know the difference between the whole Vec an element within the vec. Therefore it treats any mutation as one that could potentially invalidate anything with the same lifetime and doesn't compile. So I believe the plane model to be strictly better because it allows for this and still prevents the real scary thing:
let x = vec![1, 2]; let a = &mut x[0]; x.push(3); a = a + 1;
[–] 0c3ca83 3 days ago
[–] jordan_bonecut 3 days ago
[–] jordan_bonecut 3 days ago
[–] 0c3ca83 3 days ago