3 ms·
TLA+ = formal language for modeling software above the code level and hardware above the circuit level by Leslie Lamport (of vector clock and Paxos fame, among
by hackingonempty 3mo ago
TLA+ = formal language for modeling software above the code level and hardware above the circuit level by Leslie Lamport (of vector clock and Paxos fame, among other things.)
https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html
- mike_hock 3mo agoSo there's \in, \subseteq and probably many others that are written just like in Latex. Notably \cap and \cup were also copied from Latex, which describe the shape of the symbol instead of its meaning. But not \to, \mapsto, \Vee and \Wedge, they're written as ASCII art ->, |->, \/ and /\. Then there's SUBSET, which means power set ... yeah. -_-
- groovy2shoes 3mo agoLeslie Lamport is also the original creator of LaTeX.
- bch 3mo agoWhere LaTeX[0] is the collection of Lamports macros over Knuths[1] TeX[2]. [0] https://en.wikipedia.org/wiki/LaTeX https://en.wikipedia.org/wiki/LaTeX [1] https://en.wikipedia.org/wiki/Donald_Knuth https://en.wikipedia.org/wiki/Donald_Knuth [2] https://en.wikipedia.org/wiki/TeX https://en.wikipedia.org/wiki/TeX
- igornotarobot 3mo agoIf the LaTeX-like syntax worries you, several projects aimed at providing PL-like syntaxes for TLA+. They vary by their degree of how much of the logic they throw away. I am not going to advertise these projects here, but you would find them on GitHub search by typing the tags like "#tlaplus #language", "#tlaplus #library", and "#tlaplus #pluscal".
- mike_hock 3mo agoNo, I just find the inconsistent syntax annoying, but it turns out most things have alternative Latex-style spellings. I just went by their examples.