Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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.


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/ (direct link to spec: http://www.procode.org/cachespec/CacheSpecv1.pdf). The syntax is quite beautiful, and almost immediately familiar to anyone who knows standard mathematical notation.


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!




Consider applying for YC's Fall 2025 batch! Applications are open till Aug 4

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: