Redex takes this in an interesting direction, allowing you to write your language models in S-expressions, run them, test them, and get LaTeX out automatically. See https://redex.racket-lang.org/ and https://eecs.northwestern.edu/~robby/lightweight-metatheory/... .
It's true that the language of mathematics was optimized for a different medium: written formulas on paper. Algorithms are better expressed in pseudo-code, but to describe the exact effects of a language instructions we have to resort to formal semantics (whether denotational, operational or axiomatic), which basically describe the workings of a virtual machine in terms of a temporal logic expressed with mathematical symbols.
The ellipsis in maths is usually an ambiguous symbol whose meaning changes depending on context. In CS, it typically represents either vectors in memory or successive recursive calls. Trying to provide a precise meaning for its usage is a legitimate endeavor; it appears that Steele is using symbols from vector maths to achieve it. What I get from skimming the video is that the combination of overlines and underlines would be a way to represent how you would combine your nested loops in imperative programming to traverse the data structure.
Edit: have I mentioned that I'm wowed by this?!
It was a main focus of Fortress (https://en.wikipedia.org/wiki/Fortress_(programming_language...), for example, which was interesting but never quite got off the ground in the same way as other competitors, in part because of the focus on notation implementation.
If anything, my experience following Fortress led me to believe what Steele was discussing in his talk is both a tremendous opportunity but also much more difficult than the impression he creates.
For what it's worth, I thought the talk was really interesting and I would like to see it taken more seriously, if not as an immediate goal, then a long-term one.
(Source: I wrote the first parser for Fortress, as well as the first type checker and interpreter.)
I read a lot of programming language papers, but not type theory papers.
It definitely seems like there is a problem, but solving it would probably only help me a little. That said, I hope that people listen to what he has to say, because it seems very well-considered.
I think his overall point is meant to be serious though: that the language of formal CS should be more consistent.
- Computer science papers have this ad-hoc, ever evolving notation that started out in mathematics, that is not well defined (every paper ends up using a different flavour, sometimes even a bunch of mutually contradicting flavours at the same time), and that is subject to weird evolutionary pressures (like page limit of CS papers leading to extreme conciseness).
- Particularly interesting is the evolution of overline notation, and the ubiquitous but never defined use of ellipsis.
- Guy thinks this is a mess and should be cleaned up. His first contribution is solving overline notation abuse by introducing underlines, which cancel out overlines, thus implementing quasiquoting in mathematical notation. His second contribution is formalizing the meaning of ellipsis by defining a transformation from ellipsis form into over/underline form.
Maybe it's because of the way he presented it, or maybe because of my unfamiliarity with the space, but overall this talk really felt like a one-hour long practical joke aimed at CS academics.