3 ms·

> it's what Amazon and Microsoft uses That's not true. TLA+ is very useful but only few services adopt and benefit from it. Also it's not very readable and can

> it's what Amazon and Microsoft uses That's not true. TLA+ is very useful but only few services adopt and benefit from it. Also it's not very readable and cannot document many design aspects e.g. the reasons behind technical decisions.

agentultra 8y ago
Ok, some teams at Amazon: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... 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.
- qznc 8y ago
  Have a look at the Arc42 template [0] which is a generic outline for software architectures. TLA does not make sense for most of the items there. [0] https://arc42.org/overview/ https://arc42.org/overview/
  - pron 8y ago
    It makes a lot of sense for 1, 2, 3, 6, 7 and 12.
- sagichmal 8y ago
  > 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.
  - agentultra 8y ago
    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+. It’s a matter of degrees.
    - sagichmal 8y ago
      > For some of the Amazon engineers mentioned in the paper that training took 1 to 2 weeks. That's obviously a lie.
  - pron 8y ago
    > 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.
pron 8y ago
> TLA+ is very useful but only few services adopt and benefit from it. It's true that formal specifications are rarely used, but I would bet that the ratio of those that benefit significantly from them to those that use them is far greater than many other, far vaguer tools. > Also it's not very readable That depends on what you mean by "readable." A prose description can appear readable in the sense that the reader may think they understand what the document says, but sometimes that's just because the text is vague enough to allow for conflicting interpretations. TLA+, on the other hand, is precise. True, it takes some learning, but it's easier to learn than a programming language, as it's much, much smaller (the reference documentation for the entire language and all of the standard library fits comfortably on 7 pages (https://lamport.azurewebsites.net/tla/summary.pdf https://lamport.azurewebsites.net/tla/summary.pdf) > and cannot document many design aspects e.g. the reasons behind technical decisions It can document some decisions very well. For one, you can state precisely your assumptions as well as the requirement. You then describe the desired operation of the system. You can then check that the design fits the requirements given the assumptions, and show that other designs don't. It is true that it's not intended to model the reasoning behind every decision, such as cost/time of implementation, but generic (i.e., non-software-specific) project management tools can help you with that. Now, I am not saying that a formal specification is always required, and I agree that writing down an informal one is far better than not writing down anything at all, but it can really save a lot of time and trouble in subtle/complex/unclear cases.

agentultra 8y ago

Ok, some teams at Amazon: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... 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.

qznc 8y ago
Have a look at the Arc42 template [0] which is a generic outline for software architectures. TLA does not make sense for most of the items there. [0] https://arc42.org/overview/ https://arc42.org/overview/
- pron 8y ago
  It makes a lot of sense for 1, 2, 3, 6, 7 and 12.
sagichmal 8y ago
> 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.
- agentultra 8y ago
  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+. It’s a matter of degrees.
  - sagichmal 8y ago
    > For some of the Amazon engineers mentioned in the paper that training took 1 to 2 weeks. That's obviously a lie.
- pron 8y ago
  > 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.

pron 8y ago

> TLA+ is very useful but only few services adopt and benefit from it. It's true that formal specifications are rarely used, but I would bet that the ratio of those that benefit significantly from them to those that use them is far greater than many other, far vaguer tools. > Also it's not very readable That depends on what you mean by "readable." A prose description can appear readable in the sense that the reader may think they understand what the document says, but sometimes that's just because the text is vague enough to allow for conflicting interpretations. TLA+, on the other hand, is precise. True, it takes some learning, but it's easier to learn than a programming language, as it's much, much smaller (the reference documentation for the entire language and all of the standard library fits comfortably on 7 pages (https://lamport.azurewebsites.net/tla/summary.pdf https://lamport.azurewebsites.net/tla/summary.pdf) > and cannot document many design aspects e.g. the reasons behind technical decisions It can document some decisions very well. For one, you can state precisely your assumptions as well as the requirement. You then describe the desired operation of the system. You can then check that the design fits the requirements given the assumptions, and show that other designs don't. It is true that it's not intended to model the reasoning behind every decision, such as cost/time of implementation, but generic (i.e., non-software-specific) project management tools can help you with that. Now, I am not saying that a formal specification is always required, and I agree that writing down an informal one is far better than not writing down anything at all, but it can really save a lot of time and trouble in subtle/complex/unclear cases.