Oops, I still don't understand. With linear types, you don't have any aliasing so I don't see the value for borrowing. (maybe I'm misunderstanding the idea behind linear types?)

Seems to me, perhaps wrongly, that since there is no aliasing and values are always used, once a value is not returned by a function to be consumed, it's lifetime has effectively ended. So it's automatic?

The point I was making about ssa, dfa, etc. was that it was putting these aspects into userland via the type system.