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 simple 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 document, and you can see the list of proposed symbol translations (nicely formatted by github!) in the .csv in that directory.