how does that prevent use after free? pretty sure your algorithm is either very poorly explained or doesnt' actually work.

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

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