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.
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.