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.