This is interesting and somehow neat, but how sound is it?

Lifetimes are based on affine types, which have some proven mathematics backing their properties. This is what guarantees the absence of invalid references, the fearless concurrency, etc.

What is backing the place-based system, and what formally proves that it always works?

Can Dada put a value on the stack and pass any sort of mutable reference to it to a function? I don’t know the syntax, but maybe:

    let x: given i32 = 42
    f(x.mut)
    // now x == 43

If all permission variants of a type are shallowly laid out like the raw type, then x and x.mut are literally 32-bit integers, so how does one mutate it from a function body? A special boxed i32?

I believe places are a much better model than lifetimes, but there are challenges not discussed in this post. Ex: what would a linked list’s definition and methods look like? How does Dada handle mutation and deallocation?

I think this is a bit similar to Mojo's origin types: https://docs.modular.com/mojo/manual/values/lifetimes/#origi...