A natural question one might ask is why we prefer the term region to lifetime for discussing our semantics. To a Rust programmer, the term "region" might be completely unfamiliar (perhaps outside of a bit of poking in the compiler), and to a researcher, the terms might seem exactly the same. I'll quickly address both concerns.
In Rust programs, we often use the term "lifetimes" to refer to lifetime variables which we use
to place constraints on the concrete lifetimes of real values. In this sense, we're conflating the
real temporal notion of a lifetime with the constraints about it. So, we wish to separate these
concerns when talking about oxide. We say that every value is in its own region and that a
lifetime corresponds to the span from when a region is created to when the region is destroyed.
Lifetime variables don't appear in the core semantics of oxide because the constraints that they
imply are used in the placement of region creation and destruction.
One may also wonder where the "borrow checker" is. We've given regions their own notion of
ownership, and so all of the type checking related to region creation and destruction is exactly
the mechanisms of borrow checking. Rather than generate and later solve constraints as in rustc,
we check that our ownership discipline is maintained throughout type checking.
It seems to me that the term "lifetime" is often conflated with the term "region" for historical reasons. The separation we wish to draw is that we infer and discuss lifetimes as a method of realizing regions. That is lifetimes are a temporal property of a value (that something lives from when it is allocated to when it is deallocated), and regions are the concrete realization of where that data is allocated and deallocated.