On Thursday, September 9, 2021 at 10:06:41 PM UTC+2 andrew...@xxxxxxxxx wrote:
I'd like to get peoples' thoughts on this. Currently, the TLA+ tools only accept ASCII TLA+. ASCII TLA+ is also what I spend my time looking at while I'm writing TLA+ specs. However, it would be neat to have the ASCII symbols translated into their Unicode math equivalents in real time as I am typing, similar to Mathematica (if you've ever used that). I hope to get a demo of this up and running for my talk at the TLA+ conference at the end of September. To that end, I've added support for unicode symbols to the TLA+ tree-sitter parser and am writing a simhttps://github.com/tonsky/FiraCodeple utility to translate TLA+ files from ASCII to Unicode and back as a prelude to getting the real-time translator working (probably as a Neovim treesitter module). I should mention Unicode TLA+ is an old idea, dating back at least five years to Ron Pressler's work trying to get SANY to support Unicode, and maybe as early as Specifying Systems where Leslie speculates that some non-ASCII TLA+ version might come along in the future. I've fleshed out a TLA+ Unicode proposal (with discussion of design decisions and drawbacks) in this https://github.com/tonsky/FiraCodedocument, and you can see the list of proposed symbol translations (nicely formatted by github!) in the .csv in that directory.Some questions to provoke discussion:
- Do you believe you would personally find it useful/easier to see TLA+ specs in their Unicode form as you are writing them?
Yes. It could be very useful indeed.
I currently use https://github.com/tonsky/FiraCode and that works pretty well.
Maybe FiraCode can be hacked to handle \in, \E, \A etc. It handles arrows, /\, \/, ==, <> etc.
Example,
- If you are a non-English user, would you find it useful to be able to use non-ASCII characters in identifiers (operator/module/function names, etc.) or strings?
Not really. I tried it in golang and things get ugly. See also Turing's paper https://londmathsoc.onlinelibrary.wiley.com/doi/pdf/10.1112/plms/s2-42.1.230.
It has symbols that I can't name so things get hard to understand.
- Do you agree with the Unicode symbol choices or have any suggestions?
Andrew