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