Also it's not very readable and cannot document many design aspects e.g. the reasons behind technical decisions.
Not very readable? How so? I'd rather read a concise mathematical definition rather than three pages of prose and diagrams. It is most definitely readable although it does require some training to understand the mathematics if you're not used to reading it. Just as reading a blueprint requires a bit of training.
You can write prose into your specifications and integrate the outputted PDF specifications with the rest of your documentation.
> Not very readable? How so? I'd rather read a concise mathematical definition rather than three pages of prose and diagrams. It is most definitely readable although it does require some training to understand the mathematics if you're not used to reading it. Just as reading a blueprint requires a bit of training.
You glibly toss off "a bit of training" as if it's an afternoon's work over a cup of coffee. Understanding, intuitively, the systems that mathematical models like TLA describe is _extraordinarily_ difficult. Reading that 1-page model description for comprehension could be the work of days. Reading a 10-page prose and illustration description of the same system is likely to be the work of 10 minutes, and result in a much more thorough practical understanding of the system.
> Understanding, intuitively, the systems that mathematical models like TLA describe is _extraordinarily_ difficult.
It is the opposite of intuitively extraordinarily difficult. It is much easier and more intuitive than understanding code. It is, however, different from code, so your coding skill do not automatically transfer to TLA+, but developers are generally able not only to read but to write TLA+ specifications of complex systems after a 3-day workshop or about 2 weeks of part-time self-study. Learning TLA+ is far easier than learning a new programming language, and it is much simpler than any programming language in existence. The difficulty is not at all with intuition, but with unfamiliarity. In any event, reading TLA+ is much, much, much easier than writing/understanding the systems for which you use TLA+ for.
For some of the Amazon engineers mentioned in the paper that training took 1 to 2 weeks.
The trade off for that training is that you know the those properties it describes are correct. For some systems the trade off is worth it and for a few, required.
I didn’t say you should use TLA+ for simple projects. It is incredibly useful for specifying systems where correctness, liveness, etc matter greatly and the complexity of the project is sufficiently high that you’d be uncomfortable describing it with boxes and arrows.
I think it’s rather reckless to design a complex system of the sky-scraper magnitude without some sort of verification tool like TLA+.
You can write prose into your specifications and integrate the outputted PDF specifications with the rest of your documentation.