1. 13

  2. 11

    This article inspired me to try TLA+ and adopt it for use in my distributed systems class. Here are two posts I discussed this process: http://muratbuffalo.blogspot.com/2014/08/using-tla-for-teaching-distributed.html http://muratbuffalo.blogspot.com/2015/01/my-experience-with-using-tla-in.html

      1. 4

        Leslie Lamport’s “Who Builds a House without Drawing Blueprints?” http://cacm.acm.org/magazines/2015/4/184705-who-builds-a-house-without-drawing-blueprints/fulltext is something of a companion to this. I don’t like Lamport’s chosen analogy, but agree with his overall point.

        One interesting thing about Lamport’s approach (and the TLA+ approach) is the simple mathematical basis. By choosing set theory and predicate logic, I think he’s made a tool that’s easier to approach theoretically than those based on other formalisms (like Pi calculus and type theory). That’s both a strength and weakness, so it will be interesting to see how this evolves in the future.