In which Guy looks at 25,000 pages of paper published in POPL, PLDI, OOPSLA, ICFP, PPOPP, gives a history on notation of inference rules, BNF, Regular Expressions, encounters over 20 different ways of denoting variable substitution [0]. It’s a lengthy, deep, eye-opening research into a language no one really invented but just became widely used by researchers.

[0] I theorize that all these different forms arose because writers couldn’t find the right TeX macro