On Marketing Formal Methods
Hi everyone!
Back from vacation! Spent most of it cooking. Check out this beauty:
Bottom layer is a dark chocolate and peanut butter ganache, top layer is a raspberry agar gel. Okay that's enough not computer things
Marketing Formal Methods
The past year I focused on FM for developers: making it accessible and exciting. That's good for the overall health of the formal methods community. But I'm also trying to run a business, and devs don't decide budgets. I need to appeal to managers and CTOs. Which is a problem, since I don't know anything about sales. Like is my "this is great but has flaws" shtick a bad idea? It works really well with developers, but do CTOs want to hear "this will solve EVERYTHING"? Dunno.
Okay, so here's what I'm thinking to start. CTOs want to save money. FM provides two benefits: it gives you a better understanding of the system, and it catches bugs. The first is way too nebulous to pitch. So we have to focus on "catching bugs".
Problem: most people, including devs, think bugs aren't a big deal. They're thinking of bugs like "the date's wrong" or "you have to click twice." Bugs as background noise, low-grade annoyances that are constantly coming and going. Which makes sense, most bugs are like this. FM doesn't look like it saves much money here. You're investing time now to save time later. It's not clear that you'll net a profit in that trade. Less so when you're paying for training.
So we want to focus on bugs that piss people off. Bugs that can actually cause a loss in business value. Where not fixing the bug is directly costing you money and losing customers. These kinds of bugs are much rarer, but even one is Very Bad. I need to focus on companies with these kinds of bugs and convince them that FM in particular will help them.
So pitch: FM helps you catch complex, subtle, dangerous bugs:
- Complex: lots of steps to reproduce, easy to introduce in the design-phase, and hard to test for
- Subtle: no obvious signs it's there, hard to notice in QA, might be latent in production for a while
- Dangerous: violates core business assumptions, "drop everything and fix" when you find out about it
Example of this all is my Trading Platform TLA+ spec. It has a bug where it's possible to "steal" an item from another person. It's an expensive bug:
- Complex: takes three people and four steps to trigger
- Subtle: no stack trace, no crashing, it's just that an item mysteriously disappears from your inventory
- Dangerous: people are suddenly losing items, huge abuse potential, you have no idea how long it's been going on
Your testing won't find it, your QA won't find it, your monitoring won't find it. Better use TLA+ then.
I also need to show that FM is a cheap investment. So emphasize that it works with legacy systems and with any codebase. Finally, show testimonials that other companies have saved a lot of money with it. Nobody gives hard numbers of "dollars saved", but there are still some high-profile cases I can lean into. How long does a case study need to be?
That takes care of making the pitch. I need to put it in front of the right people. AKA people who already believe that their business is vulnerable to expensive bugs. I think this would be cloud infra, B2B tech companies... there's probably a lot of other industries I'm not seeing. One limitation people might not expect: the companies most serious about correctness are the ones who need end-to-end verification, which isn't what I do. So they need to be afraid of bugs, but not TOO afraid of bugs.
Really the bigger problem here is getting in front of these people. Is cold-calling a good idea? That doesn't seem like a good idea. Better idea: ask devs who like my work to get me meetings with their bosses.
Short term priority: write "Formal Methods Will Save You Money". Make pitch materials to show people. Update my consulting page with better stuff. Get testimonials from previous clients. Longer term: build a bigger network of decision-makers. Harass my friends in business school.
Miscellaneous Formal Methods Links
- Alloy4Fun: You can now try Alloy online!
- tlaplus_jupyter: You can now try TLA+ online! And in a Jupyter notebook. But also online.
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.