5 ms·

I also took the under bar suggestion as a joke/troll. He mentioned horizontal lines don't work well with OCR earlier in the talk. He also said parenthesis based

I also took the under bar suggestion as a joke/troll. He mentioned horizontal lines don't work well with OCR earlier in the talk. He also said parenthesis based syntax worked better for typesetters, which I feel still holds true with LaTeX. I think his overall point is meant to be serious though: that the language of formal CS should be more consistent.

kd0amg 9y ago
Underline seems like a perfectly sensible thing to me. I've run into problems like his "same Γ, different x and τ" example many times. In PLT Redex, I have to either make sure the thing I intend to be non-subscripted is already bound elsewhere or make an after-the-fact check that all of the subscripted versions of it are equal. Both options are awkward, and which one I have to do varies by situation. An `unsequence' notation to complement the `sequence' notation (which is actually done in Redex by appending an ellipsis) would let me directly say what I mean. The OCR issue is strictly an aspect of the marks put on the page rather than the ideas they describe, and a completely serial notation could be used as well (similar to backtick and comma for quasiquotation).