> We also haven’t checked any of the metatheory, so this could all be fatally flawed!
What I think makes the most sense is to have a nested hierarchy of type universes:
(0) All types
(1) Types that support sharing (data structures, first-class functions, but not ephemeral resources)
(2) Types that support equality testing (data structures not containing first-class functions)
Standard ML already has a similar hierarchy, but levels (0) and (1) are collapsed into a single one. At least it is intuitively obvious that this isn't wrong. The type safety proofs can come later.
Also, I'd rather not have a notion of borrowing at all. It's fine for Rust, because it's a low-level language. But, in a high-level language, if you want to share data structures, just use garbage collection. And, if you really want to share mutable objects (which most of the time you shouldn't), use mutexes. Mutexes themselves don't exactly support sharing, but they can be explicitly cloned and locked.
Idris programming language has "Uniqueness types" [1], that are inspired by Clean and Rust.
There is also an interesting talk [2] where Idris author discusses state/side-effects management.
[1] http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...
[2] https://www.youtube.com/watch?v=kpPyolN65s0