"TLA+ Helps Programmers Squash Bugs Before Coding"

Design is an integral component of the development process for most software engineers. A programmer devises algorithms to support their code and constructs models to visualize how the various parts of their systems will function together, similar to an architect drawing blueprints. Programmers should be able to test these algorithms and models in order to identify design flaws before they become bugs in the written code. This is the goal of TLA+, an open source, high-level language for modeling software programs and hardware systems. The logic behind it is based on the Temporal Logic of Actions (TLA), a mathematical technique for reasoning about the correctness of concurrent algorithms. Leslie Lamport, a distinguished scientist at Microsoft Research who is best known for inventing LaTeX, a document-preparation system for scientific papers, created both TLA and TLA+. Lamport notes that TLA+ is a specification language, not a programming language. He explains that it describes the program at a higher level of abstraction—what it is intended to do and how it is supposed to do it. Therefore, TLA+ is useful for verifying the validity of a program's design or supporting algorithm, a capability made possible by the TLA+ model checker. After developing specifications and writing models on TLA+, engineers can use the model checker to detect and correct design errors prior to implementing code. This article continues to discuss TLA+ helping programmers address bugs before coding. 

IEEE Spectrum reports "TLA+ Helps Programmers Squash Bugs Before Coding"