Creatively Misusing TLA+
I spent the past few weeks thinking about complexity and poking dead birds and stuff, but now that the March TLA+ workshop is available (use C0MPUT3RTHINGS for 15% off!), I’m back in teacher mode and making workshop improvements.1 TLA+ is intended for finding flaws in software designs. But what else can we do with it?
Creative Misuse is the use of a tool in an unintended way. For example, if you use a screwdriver to pry something open, or a book as a monitor stand. Creative misuse in software includes making games in Excel spreadsheets and using yes to test for broken hardware. Creative misuse is 1) very fun, and 2) expands the space of how useful the tool is. I love finding creative misuses for tools. Here’s a few of them for TLA+.
In most programming languages, we construct values step-by-step. In most formal specification languages, we instead take a big set of all possible values and then winnow them down with predicates. This is less efficient, which is why programming languages don’t do it, but it’s also a lot more expressive.
