Hillel Wayne introduces TLAplus and explains how formal specification helps design and verify concurrent and distributed systems.
This video was recorded at Code Mesh LDN 18 bit.ly/2P7SPII
Get involved in Code Sync's next conference bit.ly/2Mcm4aS
---
EVERYTHING ABOUT DISTRIBUTED SYSTEMS IS TERRIBLE
by Hillel Wayne
THIS TALK IN THREE WORDS:
TLA+
Formal
Specification
TALK LEVEL: Intermediate
ABSTRACT
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.
This talk will introduce the ideas behind TLA+ and how it works, with a focus on practical examples. We'll also show how it caught complex bugs in our systems, as well as how you can start applying it to your own work.
Read the full abstract: codesync.global/speaker/hillel-wayne/
---
THE SPEAKER - HILLEL WAYNE
Coder, chocolatier, cjuggler
Hillel is a software consultant in Chicago who specialises in formal specification. He is the author of Learn TLA+ (learntla.com), currently writing Practical TLA+ (Apress, est 2018), and on the Alloy Adoption and Outreach working group. In his free time he juggles and makes candy.
More on Hillel Wayne: codesync.global/speaker/hillel-wayne/
---
CODE SYNC & CODE MESH LDN 18
Code Mesh LDN is powered by Code Sync. Code Mesh LDN 18 was sponsored by WhatsApp, Toyota Connected, Erlang Solutions, TEAMango, and aeternity.
CODE SYNC
Website: www.codesync.global
Twitter: www.twitter.com/CodeMeshIO
Facebook: facebook.com/CodeSyncGlobal
LinkedIn: linkedin.com/company/code-sync/
Mail: info at codesync.global
#CodeMesh #HillelWayne #TLA+ #FormalSpecification #DistributedSystems
Why it's here
3 people recommend this
What people say. Recommended as an engaging introduction to using TLAplus for specifying and verifying distributed systems.
Moments people linked to
p
u/pron98in r/programming • Recommends
On “Why Don't People Use Formal Methods?”
> Cause it takes an insane amount of time
So does testing and fixing design errors.
> and usually it’s benefits are not justifiable
I don't know if there is enough data to reach any conclusion, and also "formal methods" differ so much in kind that generalizing over them is a little meaningless. But we're slowly learning how to apply *some* formal methods to *reduce* the cost of building software (like Amazon's outstanding report (more here)), not just for "complicated distributed systems", but even seemingly simple software or UI design.
> Most programmers don’t know how to use the tools and must be trained.
Learning TLA^+ (or Alloy) takes less time -- as Amazon reports -- than learni…
On “Everything about distributed systems is terrible”
link to this video
>These are all great ways of dealing with concurency
>It's great to have these
>But these all have one very critical problem.
cue 26 minutes of video
It's almost as if he knew what he was talking about.
Backseat programmer much ?
