While I agree that a standardized notation would be great (though it's hard, e.g. I think e[v/x] is a lot harder to understand than e[x := v] if you've never se

While I agree that a standardized notation would be great (though it's hard, e.g. I think e[v/x] is a lot harder to understand than e[x := v] if you've never seen it before), I take issue with the idea that if people struggle with notation that it must be the fault of the notation. The author quotes a tweet about someone complaining about the notation used for a basic type judgement for being cryptic. Any introductory text will immediately cover this and looking it up, you can learn the notation (which is really rather simple) in about 5 minutes. Yet, the tweet author claims that they saw this notation 12 years ago and still can't understand it. Well, to me the only reasonable conclusion is that they simply didn't bother spending a few minutes looking it up and instead expected that they would magically understand it after enough time has passed. I seriously doubt that gammas being used instead of the word 'context' is why they're struggling. And this is my core issue with a lot of these "notation is a barrier" complaints. Instead of being valid complaints about esoteric notation (and especially using this notation without defining it!), it's people who believe that knowing how to program means you should be able to read any PL text without any preparation which is just unreasonable. If you want to seriously engage with a paper, you'll have to read up on the basics first in literally any field.