2018-12-12 Designing Distributed Systems with TLA+

Admission: Free, General Admission, open to the public

Distributed systems are hard. How do you test your system when it's spread across three services and four languages? Unit testing and type systems only take us so far. At some point, we need new tools. Enter TLA+. 

TLA+ is a specification language that describes your system and the properties you want. This makes it a fantastic complement to testing: not only can you check your code, you can check your design, too! TLA+ is especially effective for testing concurrency problems, like crashes, race conditions, and dropped messages. TLA+ is so effective for this that both AWS and Azure teams consider it essential to their work. It keeps subtle, serious bugs out of their code and helps them optimize without losing correctness. And it's not just for the cloud: engineers have used TLA+ to verify everything from business workflows to video games.

This talk will introduce the ideas behind TLA+ and how it works, with a focus on practical examples and how you can apply it to your own work.

Hillel is a software consultant in Chicago who specializes in formal methods. He is the author of Learn TLA+ (learntla.com) and Practical TLA+, is on the Alloy board, and teaches workshops on both of these languages. In his free time, he juggles and makes candy. He probably brought enough for everyone.

While there will be light refreshments available, feel free to "brown bag" it and bring in food from the outside to eat during the social hour.

Reservations:

Click here to Reserve for Wednesday, December 12

or send an e-mail to greg@neumarke.net