The compiler statically tracks “where” everything lives. It also knows “when” the “where” is valid.

Each “where” is called a plane, which is a tree. The stack plane contains all your function calls memory, a structure allocated on the stack has a child plane for each field. The compiler tags which plane something is from at compile time and tracks when it dies.

Things do get complicated in scenarios like:

fn max(a: &usize, b: &usize) -> &usize {

  if *a > *b { a } else { b }

}

In such a scenario the compiler tags the result with both of the input planes. However, you cannot define add a postcondition ensures clause to make it more precise

▲ tancop an hour ago | parent | next [-]

Sounds a lot like group borrowing from Valen, but that one still has annotations like `entity in world.entities[] mut`. Are you tracking the same things implicitly with post conditions?

▲ 0c3ca83 an hour ago | parent | prev [-]

And what about allocations and threads?

▲

jordan_bonecut an hour ago | parent [-]

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

▲

0c3ca83 37 minutes ago | parent [-]

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

	▲	jordan_bonecut 17 minutes ago \| parent \| next [-]
		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
	▲	jordan_bonecut 25 minutes ago \| parent \| prev [-]
		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