how does it make sense to utter the sentence "this has been abstracted [away]" when the `this` is itself the essence of abstraction.
i'm not really sure how people aren't getting what i'm putting down here: type theory can't be abstracted away because type theory itself is the thing that does the abstracting.
> > It’s a testament to computer science that this has been so thoroughly abstracted over the years
As your brackets indicate, you are reading a word "[away]" that is not explicitly present in the text. It seems to me to make more sense to read it without adding "away". (Wiktionary, for example, does not require that, or any, preposition in sense 6 of https://en.wiktionary.org/wiki/abstract#Verb, which is the one that seems to me to fit here.)
For example, I am a mathematician, and I could say that mathematics has been abstracted over the years (millennia!). I do not mean that the mathematics has been abstracted away, which I agree with you would be in some sense meaningless, but rather that the mathematics itself has literally been abstracted: from only being able to count and do arithmetic with specific real-world objects, to being able to do count and do arithmetic with numerals that did not refer to a specific thing, to being able to use letter to refer to numerals of unknown or variable value, to … well, there's not such a clear linear progression after that, but there's definitely a tower of abstraction. I hope that this sense of "mathematics has been thoroughly abstracted over the years" is an intelligible one (even if phrased differently from the way I assume you, or perhaps even I, might phrase it ourselves). It is in that sense that I take the sentence "It’s a testament to computer science that this [meaning, I think, notation in type theory] has been so thoroughly abstracted over the years".
1. Separated or disconnected; withdrawn; removed; apart. [First attested in the mid 16th century.]
2. (now rare) Separated from matter; abstract; ideal, not concrete.
3. (now rare) Abstract; abstruse; difficult.
4. Inattentive to surrounding objects; absent in mind; meditative.
three of these four connote the same thing as "away".
i mean what's the point of fighting so hard to make up an interpretation of this word that doesn't exist when the obvious interpretation clearly fits: this person is happy that the type theory isn't relevant anymore.
> i mean what's the point of fighting so hard to make up an interpretation of this word that doesn't exist when the obvious interpretation clearly fits: this person is happy that the type theory isn't relevant anymore.
I agree that it's probably not worth two or more people, none of whom is ljm, fighting over what ljm might have meant, but neither I nor hathawsh (https://news.ycombinator.com/item?id=37149803) reads the comment the way that you do, so I am not so sure that this is the obvious interpretation, and I am fairly sure that it is not the most charitable interpretation.
The interpretation I reference in https://news.ycombinator.com/item?id=37152933does exist, and is supported by a dictionary definition just as yours is; so, without addressing whether it is obvious or whether it fits—surely subjective matters—it is certainly a possible interpretation, just as yours is.
anything is possible, including that none of these words are actually the words we think they are and we're actually communicating across an interdimensional gateway that's doing the translation for us. it is certainly possible, but just like with which interpretation of abstracted to take, it's certainly not probable.
yes and that's exactly my point...
how does it make sense to utter the sentence "this has been abstracted [away]" when the `this` is itself the essence of abstraction.
i'm not really sure how people aren't getting what i'm putting down here: type theory can't be abstracted away because type theory itself is the thing that does the abstracting.