I was lucky enough to ask Leslie Lamport some questions about TLA+, which is a programming language of his creation based on the Temporal Logic of Actions: basi

I was lucky enough to ask Leslie Lamport some questions about TLA+, which is a programming language of his creation based on the Temporal Logic of Actions: basically predicate logic with some reasoning about Time thrown in. With it, you specify concurrent algorithms in terms of possible state transitions and assertions which should hold in all program states (or subsets of those states). A model checker then runs through all the states, checking your assertions (this can understandably take quite a while, so there's a distributed model checker for large systems). A really good takeaway from the talk is a point he made on software testing: for sequential algorithms, conventional software testing is likely to find most of the bugs you really care about. For concurrent algorithms, however, finding those bugs through software testing is extremely unlikely; an Amazon paper on TLA+ usage[0] details a bug found which required a 35-step trace to reproduce. Given the speed of computers today, it's only a matter of time before these bugs are hit and your system implodes in a confusing and impossible-to-reproduce way. Software testing by itself just isn't good enough anymore. [0] http://research.microsoft.com/en-us/um/people/lamport/tla/amazon.html http://research.microsoft.com/en-us/um/people/lamport/tla/am...