3 ms·
I liked the article and tried to look into TLA+, but the documentation is off-putting at every turn. There is no HTML documentation, you need to download a ZIP
by StavrosK 6y ago
I liked the article and tried to look into TLA+, but the documentation is off-putting at every turn. There is no HTML documentation, you need to download a ZIP of a book. Opening the ZIP, it's not just a single PDF, it's a bunch of PDFs (many a page or paragraph long) that the table of contents hyperlinks to. This makes impossible to skim the documentation.
Looking at some examples, it looks like TLA+ uses non-ASCII symbols which are then maybe mapped to ASCII? As such, you need to remember lots of obscure sigils, and I couldn't find a high-level intro of how it works.
It sounds very interesting, but the documentation could be made much more helpful. Lamport comments that "people nowadays don't read, so I made a video course", but I'm not surprised people don't read if reading is this hard. (I personally dislike video courses because you can't skim them and would much prefer HTML documentation).
- grndn 6y agoAgreed about the TLA docs, but it is worth persisting, as TLA is very useful in some situations. These slides cover the basic syntax enough to get started. https://www.slideshare.net/ScottWlaschin/tla-for-programmers-235339832 https://www.slideshare.net/ScottWlaschin/tla-for-programmers...
- StavrosK 6y agoThank you, that's very useful.
- hwayne 6y agoI wrote an online guide designed to be a bit more accessible: https://www.learntla.com https://www.learntla.com (I stopped working on it to write a full book, but now that that's done I really need to get back and overhaul it. Still a useful resource IMO)
- StavrosK 6y agoThis is really well done, thank you. It's so well done that I'm reading just because it's so interesting, I was afraid my eyes would glaze over but I'm really engrossed by how you're qualifying the problem first.