3 ms·

How Amazon Web Services Uses Formal Methods

6 points by tim_sw 11y ago

gravypod 11y ago
Can someone break down these buzz words? What is a "Formal Method" in laymen terms? How do they differ from other method documentation techniques? Why should I change the way I communicate my specifications, what are the benefits?
- greenyoda 11y ago
  If the specs are written in a language that can be understood by a computer, the computer can be used to prove assertions about the spec (will it function correctly? does it contain any internal inconsistencies?). More information on formal methods can be found here: https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods The formal specification language referenced in the article, TLA+, is described here: https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B Here are some interesting comments from an earlier submission of this article: https://news.ycombinator.com/item?id=8096185 https://news.ycombinator.com/item?id=8096185
  - gravypod 11y ago
    So it's doctest [0] from python? Is the testing framework at amazon open sourced? I really like doctest and wish there were more implementations of this for other languages. If not, than that is unfortunate. If I can't see the implementation of something, then I don't really consider it "tangible," so that makes a lot of this "academic-enriched" information unusable for me. [0] https://docs.python.org/2/library/doctest.html https://docs.python.org/2/library/doctest.html
    - greenyoda 11y ago
      From the description, doctest seems more like a kind of unit test: it makes sure that the test cases embedded in the doc string return the correct values when run. But you can't prove that the a function works correctly just by running a few test cases (or even a lot of test cases) - doctest has no representation of the function, so it can't reason about how the function is supposed to work (let alone the system as a whole). For example, it can't tell if the arguments passed to this function by another function will always conform to what this function expects to receive.
      - gravypod 11y ago
        No, you never can. In any language, no matter the kind of specification, I can write an elaborate method to break any form of non-human verification. Maybe I'm not getting it. It just sounds like a unit test design with extra steps. I might just need to see an example to understand how it works. Too bad this is closed source.
        greenyoda 11y ago
        The TLA+ tool that they're using is actually open source. You can read about it here (and there's a link to the source on CodePlex): http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html http://research.microsoft.com/en-us/um/people/lamport/tla/tl...

6 points by tim_sw 11y ago

Can someone break down these buzz words? What is a "Formal Method" in laymen terms? How do they differ from other method documentation techniques? Why should I change the way I communicate my specifications, what are the benefits?

greenyoda 11y ago
If the specs are written in a language that can be understood by a computer, the computer can be used to prove assertions about the spec (will it function correctly? does it contain any internal inconsistencies?). More information on formal methods can be found here: https://en.wikipedia.org/wiki/Formal_methods https://en.wikipedia.org/wiki/Formal_methods The formal specification language referenced in the article, TLA+, is described here: https://en.wikipedia.org/wiki/TLA%2B https://en.wikipedia.org/wiki/TLA%2B Here are some interesting comments from an earlier submission of this article: https://news.ycombinator.com/item?id=8096185 https://news.ycombinator.com/item?id=8096185
- gravypod 11y ago
  So it's doctest [0] from python? Is the testing framework at amazon open sourced? I really like doctest and wish there were more implementations of this for other languages. If not, than that is unfortunate. If I can't see the implementation of something, then I don't really consider it "tangible," so that makes a lot of this "academic-enriched" information unusable for me. [0] https://docs.python.org/2/library/doctest.html https://docs.python.org/2/library/doctest.html
  - greenyoda 11y ago
    From the description, doctest seems more like a kind of unit test: it makes sure that the test cases embedded in the doc string return the correct values when run. But you can't prove that the a function works correctly just by running a few test cases (or even a lot of test cases) - doctest has no representation of the function, so it can't reason about how the function is supposed to work (let alone the system as a whole). For example, it can't tell if the arguments passed to this function by another function will always conform to what this function expects to receive.
    - gravypod 11y ago
      No, you never can. In any language, no matter the kind of specification, I can write an elaborate method to break any form of non-human verification. Maybe I'm not getting it. It just sounds like a unit test design with extra steps. I might just need to see an example to understand how it works. Too bad this is closed source.
      - greenyoda 11y ago
        The TLA+ tool that they're using is actually open source. You can read about it here (and there's a link to the source on CodePlex): http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html http://research.microsoft.com/en-us/um/people/lamport/tla/tl...