And that's not really sufficient; words have a life of their own and take on contextual meanings outside of whatever scope they're introduced in. Case in point, linear types come from linear logic, by Girard, whereas relevant types come from unrelated older work by Belnap and Anderson. The simple act of putting them under one umbrella term, "substructural types", erases the older work and means that the article will focus more on Girard's perspective of logic.
Then the article makes the "discovery" that "People who say they want Linear™ Types In Rust actually just want Proper Support For Relevant™ Types.", which is pretty obvious if you know this historical context, and coins yet another term, must-use types, which unsurprisingly has no ™ after it.
I think I get what you're trying to do, I myself used ™ for a little bit back 6-7 years ago, a little bit before I wrote http://insearchoftheultimateprogramming.blogspot.com/2011/04.... But ™ just isn't effective; even if you think you know what a term means, you can't explain it except by its relationship to other terms. And once you forget what that ™ symbol referred to you're just as clueless as everyone else. Whereas URLs are "resource locators" and actually clarify what you intended.
The bit about erasing seems like a bit of stretch. Belnap taught at least one of his proof theory classes using Restall's "An Introduction to Substructural Logics" as a textbook. (Belnap did make it clear that he didn't think linear logic was relevant to his own philosophical concerns, but that's not the same as saying he bears it some kind of ill-will).
Well, if relevance logic is part of linear logic, and it's a true subsumption relationship, then you're saying Belnap doesn't think relevance logic is relevant anymore. So in other words he's pretty much rejected logic altogether.
I guess it makes sense, his most recent papers are about indeterminism (http://www.pitt.edu/~belnap/futurecontingents.pdf), which logic doesn't handle well, but I'm not quite sure how you'd represent the branching-universe model he uses in a type system. I guess you'd need the history operator he uses, m/h = moment m on history h.
I was referring to the subsumption under substructural logic, not a subsumption under linear logic. Belnap seemed to view linear logic as rather different from his own interests in relevance logic.
Then the article makes the "discovery" that "People who say they want Linear™ Types In Rust actually just want Proper Support For Relevant™ Types.", which is pretty obvious if you know this historical context, and coins yet another term, must-use types, which unsurprisingly has no ™ after it.
I think I get what you're trying to do, I myself used ™ for a little bit back 6-7 years ago, a little bit before I wrote http://insearchoftheultimateprogramming.blogspot.com/2011/04.... But ™ just isn't effective; even if you think you know what a term means, you can't explain it except by its relationship to other terms. And once you forget what that ™ symbol referred to you're just as clueless as everyone else. Whereas URLs are "resource locators" and actually clarify what you intended.