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?
Quite a lot of type system modeling has gone into Dada so far, though I don't know the details. Some of that work is here: https://github.com/dada-lang/dada-model
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?
Quite a lot of type system modeling has gone into Dada so far, though I don't know the details. Some of that work is here: https://github.com/dada-lang/dada-model
I think this is a bit similar to Mojo's origin types: https://docs.modular.com/mojo/manual/values/lifetimes/#origi...