Right or wrong, simply saying something is poorly named doesn't show that someone is hostile towards academia. By that standard, most of the academics I know would be hostile to academia, since they invariably think something in their field has a bad name.
I'm just miffed that they're complaining about names that are actual words. How would you like if they were all named after their discoverers, and therefore an a priori undistinguished mishmash of proper names? (cf. separation axioms[1])
That's pretty funny. I'm sure memorizing the differences between the Hausdorff, the completely Hausdorff, the regular Hausdorff, the normal Hausdorff, the completely normal Hausdorff, and the perfectly normal Hausdorff must be fun.
It doesn't help to use "actual words" when those words have no discernible relationship to their usage. And I don't just mean "common" usage, but the usage by others in related fields. "affine" and "linear" are commonplace concepts in mathematics, but it is in no way clear how they relate to type systems, let alone what properties a type system has when described as such.
The only other fields I know of where things are as badly named are are abstract algebra (ideal, ring, module) and grammar (infinitive, perfect, accusative). It seems to be no coincidence that type theory straddles the two.
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.
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.
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.
Gankro has a... distinctive writing style. :) He also has a master's in computer science, so if he actually has any enmity for academia it might very well be justified. :P
What I find asinine is that the writer says substructural type systems (the concept which the names of the types are inherited from) are badly named, yet I'm somewhat dubious that he knows anything about them? I certainly don't, and although the relationship between affine types and affine spaces is not immediately obvious to me, the relationship between linear types and linearity is very clear.
Hostility towards academia check
Anyway it's fine not to have proper linear types in Rust, but I don't think linear types are the enemy here.