SoftwareGR Presents Hillel Wayne: "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.

About Hillel Wayne

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 not bring enough for everyone and is very sorry about that.