[wtallis]

Those are stupidly irrelevant examples. Nobody's suggesting that you would need to have a Coq parser between your keyboard and your display. You can type an incomplete or invalid expression just as easily as you can write one, but only with a computer can you have your statements automatically and reliably checked and errors flagged in realtime.

[j2kun]

Essentially, that is the argument. If the point is to allow students to manipulate the lecture as data, then it must be error-free. That is literally putting a parser between the lecturer and the students.

And your condescending comment does not address my point, which is that a lecture would not benefit from (and is actively harmed by) the "features" being suggested. Real time error flagging would be extremely distracting, and writing mathematics as source code would be tediously slow and again distract from the point of understanding the mathematics.

[wtallis]

Enabling multiple users to interact with the equations in realtime as they are being written is hardly the only possible benefit of using computers to communicate math, and even so it only requires that the equations be tokenized to be manipulable, not that the whole expression be completely error-free and the parser be running in an enforcing mode.

And your claim that writing mathematics as source code is too slow is very much lacking in proof. All we can say with confidence is that syntax like LaTeX markup on a standard keyboard layout is too inefficient for realtime use. This does not mean that realtime use is impossible if you allow for a more complicated IME and for a different final notation on-screen than the current standard math notation.

[j2kun]

I'd like to hear your ideas for other benefits.