Skip to content
Sign in
Artwork for Software Engineering Daily
Software Engineering Daily · Nov 9, 2018 · 38 min

TLA+ with Leslie Lamport

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).

0:00-38:53
Play in

transcript

No transcript — this publisher did not publish one.

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).

links2

more episodes

All episodes