TLA+ creator Leslie Lamport: 'Programmers need abstractions'

The 84-year-old Leslie Lamport is a legend. A Microsoft web page (where he once worked as a research scientist) notes that Lamport began “dabbling” in computers in the 1950s — at a time when that meant “he and a friend used to scrounge around, looking for discarded vacuum tubes to build a digital circuit.” Sixty years later, he’d received a Turing Award for “fundamental contributions to the theory and practice of distributed and concurrent systems.” After decades of research, Lamport even released his own high-level specification language in 1999 for the modeling of programs and systems, offering his own elegant way to diagram concurrency. (The TLA in TLA+ stands for “temporal logic of actions.”) But staying true to his academic origins, Lamport once quipped that the language was a “quixotic attempt to overcome engineers’ antipathy towards mathematics.” He’s serious about mathematics. After majoring in math at MIT, Lamport earned a Masters from Brandies in 1963 and a PhD in 1972. H ... Read full article.