Absolutely, I was just trying to avoid using "ownership" in my previous comment because it's more of an abstract concept than the type system and the borrow checker (which have concrete phases in the compiler, typeck and borrowck (though typeck also does more than just enforce linearity (er, affininity?))).

Maybe not completely orthogonal, but I was thinking specifically of how treatment of immutable borrows show how one could partially tack on borrowing semantics to a non-linear/affine language for at least a modicum of use-after-free protection, and also it's a common misconception that linearity ("ownership") and the borrow checker are synonymous rather than distinct-though-intertwined concepts.

You can't make a type that must be used exactly once, but you can often express that requirement in some other way. One technique is to require that some top-level function returns a value of the terminal type; then you can't accidentally abandon a computation part-way through. Here's a silly example:

https://play.rust-lang.org/?gist=b875377faa6e22b74ba8661ee10...

That little DSL lets you make multi-layer burgers, but only where bacon and patties alternate, and there is a bun on the top.