2 ms·
The syntax in that first example is off putting.
by dqpb 8y ago
The syntax in that first example is off putting.
- pron 8y agoTLA+ uses an almost-standard mathematical notation, so that people with some familiarity with mathematics can read it in ~10 minutes of training. You can see examples of what it looks like in my post here (https://pron.github.io/posts/tlaplus_part2 https://pron.github.io/posts/tlaplus_part2) This website chooses to show the ASCII version that you actually type to get the "real" pretty-printed syntax.
- jnwatson 8y agoYes, you can definitely tell the inventor of TLA was also the first developer of LaTeX. As such, it is a language best read after typesetting. For a good example, see Appendix B in Diego Ongaro's dissertation [1], the formal Raft specification. After a little of the Learn TLA+ book, I was able to muddle through the spec enough to implement it. 1: https://ramcloud.stanford.edu/~ongaro/thesis.pdf https://ramcloud.stanford.edu/~ongaro/thesis.pdf