3 ms·

Would it make sense for the TLA+ source to just be a subset of LaTeX, then? At least some fraction of the potential userbase is already familiar with that.

• pron 6y ago
  It largely already is. E.g. you can write \forall rather than \A, \lor instead of \/, \neg instead of ~, etc.. The representation most people choose to write as their ASCII typesetting source is just more ergonomic, as it's specifically tailored for TLA+; conversely, there is a LaTeX mode that renders TLA+. Anyway, it's not what you're supposed to read. The vast majority of TLA+ is readable to someone familiar with ordinary mathematical notation within two to ten minutes of training (if you know temporal logic, then almost all of TLA+ is readable within minutes). See e.g. this complete (and very sophisticated in its use of advanced TLA+) specification, written at Arm, of CPU speculation side-channels: http://www.procode.org/cachespec/ http://www.procode.org/cachespec/ (direct link to spec: http://www.procode.org/cachespec/CacheSpecv1.pdf http://www.procode.org/cachespec/CacheSpecv1.pdf). The syntax is quite beautiful, and almost immediately familiar to anyone who knows standard mathematical notation.
  • hwayne 6y ago
    This messes me up when I'm writing actual LaTeX because I keep writing `\A` instead of `\forall` EDIT: Also that spec uses a lot of really interesting techniques, such that doing a breakdown would be a good Blub study. Off to the typewriter!