Hillel Wayne
Chocolatier
Chicago, Illinois, United States
Actions
Hillel is a formal methods consultant, the author of Learn TLA+ and Practical TLA+, and a member of the TLA+ and Alloy boards. His other work includes *The Crossover Project*, a collection of interviews with traditional-turned-software engineers, and *Let's Prove Leftpad*. In his free time, he juggles and makes chocolate. He did, in fact, bring enough for everyone.
Area of Expertise
Topics
Is Software Engineering Real Engineering?
What makes software engineering different from “traditional” engineering? To find out, I interviewed 17 “crossovers”: people who have worked professionally as both a software and a traditional engineer. In aggregate, we learn three things: we are in fact engineers, we’re not actually that different as a field, and there’s a lot we can both teach and learn.
Software Modeling with TLA+
Most software flaws have one of two causes.
Sometimes the cause is that the code does not match the developer's design. Most software correctness techniques - types, tests, etc - are used to check for this issue. But other times, the code correctly implements a bad design: there is a fundamental error in the model of the system. These bugs are the most difficult to find and the most expensive to fix. Types and tests are not enough for these bugs.
The answer is software modelling. By specifying the design in a software modelling tool, developers can directly test the design for bugs without having to write any code first. Modelling software leads to simpler, safer systems built more quickly and cheaply.
One such modelling tool is TLA+. TLA+ is designed to model concurrent and distributed systems, and has successfully found bugs in everything from cloud services and message queues to video games and SSD firmware.
In this class, students will learn the basics of TLA+ from one of the foremost experts on teaching these techniques. The workshop will cover the fundamental theory of specification with several in-depth examples, and conclude with modelling a real system decided upon by the class.
Debuggable Designs with TLA+
Most software flaws have one of two causes.
Sometimes the cause is that the code does not match the developer's design. Other times, the code correctly implements a bad design: there is a fundamental error in the model of the system. These kinds of errors are often only apparent after we fully implemented the system, which makes fixing them a costly and difficult endeavor. This is especially a problem with high-performance systems, which push us towards complex designs.
With TLA+, we can directly test our designs for bugs. TLA+ is a "formal specification language", where we can encode high-level models of software systems and then analyze their behavior. TLA+ has successfully found bugs in everything from cloud services and message queues to video games and SSD firmware. After fixing the designs, developers can implement their software with more confidence and spend less time on long-term maintenance.
This session will provide a brief overview of how and why TLA+ works, and how it can be applied to find design bugs in low-latency systems.
Please note that Sessionize is not responsible for the accuracy or validity of the data provided by speakers. If you suspect this profile to be fake or spam, please let us know.
Jump to top