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.

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

The non-mobile link was much more useful for me: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext

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.