[aatd86]

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.

[Rusky]

With linear types alone you don't have any aliasing. Borrowing is a controlled way to recover some aliasing while retaining the benefits of linearity.