I wish people use "real" (pretty-printed) TLA+ syntax -- the syntax used when reading a spec -- when giving presentations rather than SANY's LaTeX-like ASCII sy

I wish people use "real" (pretty-printed) TLA+ syntax -- the syntax used when reading a spec -- when giving presentations rather than SANY's LaTeX-like ASCII syntax used to type them. The read/write ratio for maths, including TLA^+ specifications, is higher than for programs, and so there are two concrete syntaxes optimised for those two different modes. I think most people know that on the computer, maths is usually typed differently from how it's read, and they expect to read the maths, not the LaTeX source used to typeset it. It isn't any different for TLA^(+).