Tuesday, June 5, 2018
Atomic Object, 1034 Wealthy St. SE, Grand Rapids
"The Two Hardest Problems in CS"
"The two hardest problems in CS are Cache Invalidation and Naming Things." This is, if anything, too _optimistic_: cache invalidation is just a special case of concurrency, and naming things is just a special case of explaining them. And these are actually the same problem: without a way of describing concurrency, we don't have a way of understanding it, much less rigorously analyzing it.
Fortunately, we have some powerful tools to manage this. With _formal specification_, we can describe our systems in a way that's more expressive than code and more precise and unambiguous than human language. Once we have a semantics for the hard problems in CS, we have a way of studying them, finding complex bugs in systems before we've written any lines of code. We'll cover how this is useful, focusing primarily on TLA+, which is both powerful and practical enough for use in all kinds of day-to-day work.
Hillel is a software engineer and consultant in formal methods. He's currently writing a book on formal specification in TLA+ and a series on the history of UML. In his free time, he juggles and makes candy. He did, in fact, bring enough for everyone.