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 or vector’s API look like in Dada? How does it handle mutation and deallocation?

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?

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