TLA+ with Leslie Lamport
Software Engineering Daily · softwareengineeringdaily.com
Audio is streamed directly from the publisher (traffic.megaphone.fm) as published in their RSS feed. Play Podcasts does not host this file. Rights-holders can request removal through the copyright & takedown page.
Show Notes
TLA+ is a formal specification language. TLA+ is used to design, model, and verify concurrent systems. TLA+ allows a user to describe a system formally with simple, precise mathematics.
TLA+ was designed by Leslie Lamport, a computer scientist and Turing Award winner. Leslie joins the show to talk about the purpose of TLA+. Since its creation in 1999, TLA+ has been used to discover bugs in systems such as Amazon S3, DynamoDB, Xbox, and Cosmos DB.
“TLA” stands for “temporal logic of actions”, a logical system that can be used to describe the behaviours of concurrent systems.
This podcast is meant as a brief introduction of TLA+. To go deeper, check out the TLA+ website and the TLA+ video course (note: these videos are highly entertaining because of Leslie’s dry, unpredictable sense of humor).