3 ms·

You can use TLA+ -- it's what Amazon and Microsoft uses. TLA+ is a formal specification language, plain-old maths, and the tool suite includes a model checker

You can use TLA+ -- it's what Amazon and Microsoft uses. TLA+ is a formal specification language, plain-old maths, and the tool suite includes a model checker and a pretty printer. The model checker verifies properties of your specification that you want to hold true such as liveness. And it also includes a pretty-printer for exporting your specifications into well-formatted PDF documentation. The nice thing about writing specifications this way is that they are specific, at the correct level of abstraction for the problem, and can be verified. I think Lamport's analogy is apt: specifications are like blueprints. If you're building a shed in your backyard then a sketch will be sufficient. There's no need to have a blueprint. If you're building a house you'll need some kind of blueprint. The software equivalent of a sufficient blueprint for building a house is a strong, static type system, unit, integration, and property-based tests. If you're building skyscrapers you need something much more formal and I think this is where TLA+ and Lean are useful.

ex_amazon_sde 8y ago
> 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.
      - 8y ago
- 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.

ex_amazon_sde 8y ago

> 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.
    - 8y ago
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.