[bradleyjg]

Simply saying it is poorly named doesn't, but this sentence:

"Just so you can look this stuff up in The Literature, I'll be providing all these bad names with a Trademark of Disdain™, but otherwise I'd prefer to use Rust-centric terminology." pretty clearly does.

The TM thing is obnoxious.

[tpush]

I think it's it hilarious (and true that academia often chooses poor names).

[Mathnerd314]

Yeah, it would be better with coloring. Or better yet hyperlinking to the relevant Wikipedia pages / papers / memes.

Edit: pages such as https://en.wikipedia.org/wiki/Idempotency_of_entailment, https://en.wikipedia.org/wiki/Monotonicity_of_entailment, https://en.wikipedia.org/wiki/Structural_rule, https://en.wikipedia.org/wiki/Nice_guy, https://en.wikipedia.org/wiki/Linear_logic, https://en.wikipedia.org/wiki/Affine_logic, https://en.wikipedia.org/wiki/Relevance_logic (not sure why "Proper Support" is capitalized, that seems to have no referent)

Hyperlinks allow you to directly look up a term by clicking on it, i.e. are actually useful, whereas trademark symbols are just visual noise. Although of course it is possible to over-link as well, see e.g. the wiktionary FAQ on "wikifying": https://en.wiktionary.org/wiki/Help:FAQ#Wikifying, in practice this doesn't seem to happen; it's more the reverse problem of not putting in enough links.

[Gankro]

Literally the only link in the article, on the first use of the Official Terminology, is a link to the wikipedia page that defines all the terms.

[Mathnerd314]

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.

[hyperpape]

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).

[Mathnerd314]

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.

[hyperpape]

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.