How to convince engineers that formal methods is cool
Based on my experiences convincing people it's cool
Sorry there was no newsletter last week! I got COVID. Still got it, which is why this one's also short.
Logic for Programmers v0.4
Now available! This version adds a chapter on TLA+, significantly expands the constraint solver chapter, and adds a "planner programming" section to the Logic Programming chapter. You can see the full release notes on the book page.
How to convince engineers that formal methods is cool
I have an open email for answering questions about formal methods,1 and one of the most common questions I get is "how do I convince my coworkers that this is worth doing?" usually the context is the reader is really into the idea of FM but their coworkers don't know it exists. The goal of the asker is to both introduce FM and persuade them that FM's useful.
In my experience as a consultant and advocate, I've found that there's only two consistently-effective ways to successfully pitch FM:
- Use FM to find an existing bug in a work system
- Show how FM finds a historical bug that's already been fixed.
Why this works
There's two main objections to FM that we need to address. The first is that FM is too academic and doesn't provide a tangible, practical benefit. The second is that FM is too hard; only PhDs and rocket scientists can economically use it. (Showing use cases from AWS et al aren't broadly persuasive because skeptics don't have any insight into how AWS functions.) Finding an existing bug hits both: it helped the team with a real problem, and it was done by a mere mortal.
Demonstrating FM on a historical bug isn't as effective: it only shows that formal methods could have helped, not that it actually does help. But people will usually remember the misery of debugging that problem. Bug war stories are popular for a reason!
Making historical bugs persuasive
So "live bug" is a stronger rec, but "historical bug" tends to be easier to show. This is because you know what you're looking for. It's easier to write a high-level spec on a system you already know, and show it finds a bug you already know about.
The trick to make it look convincing is to make the spec and bug as "natural" as possible. You can't make it seem like FM only found the bug because you had foreknowledge of what it was— then the whole exercise is too contrived. People will already know you had foreknowledge, of course, and are factoring that into their observations. You want to make the case that the spec you're writing is clear and obvious enough that an "ignorant" person could have written it. That means nothing contrived or suspicious.
This is a bit of a fuzzy definition, more a vibe than anything. Ask yourself "does this spec look like something that was tailor-made around this bug, or does it find the bug as a byproduct of being a regular spec?"
A good example of a "natural" spec is the bounded queue problem. It's a straight translation of some Java code with no properties besides deadlock checking. Usually you'll be at a higher level of abstraction, though.
Blog rec: arg min
This is a new section I want to try for a bit: recommending tech(/-adjacent) blogs that I like. This first one is going to be a bit niche: arg min is writing up lecture notes on "convex optimization". It's a cool look into the theory behind constraint solving. I don't understand most of the math but the prose is pretty approachable. Couple of highlights:
- Modeling Dystopia about why constraint solving isn't a mainstream technology.
- Table of Contents to see all of the posts.
The blogger also talks about some other topics but I haven't read those posts much.
If you're reading this on the web, you can subscribe here. Updates are once a week. My main website is here.
My new book, Logic for Programmers, is now in early access! Get it here.