Some thoughts on the benefit of showing vs telling.
I was at PyCon last month to present on contracts and testing, and naturally the "what do you do" question came up a lot. When I mention formal methods people want me to justify why it's useful. I'm sure a lot of you have run into a similar problem, where it's really hard to explain to people why they should be writing specifications. The discussions go around in circles, where I'd raise issues like race conditions and liveness and people would object "I'd catch that with unit tests!" Most of the people who don't say that just dismiss TLA+ as purely academic.
Eventually I'd be able to convince them to sit through a quick demo. The one I use is concurrent bank account transfers: it's a relatable problem, the algorithm is extremely simple, and the invariants are intuitive. I walk them through the syntax, set up a model, and show how TLC can find a concurrency bug (nonatomic guard clauses can overdraft an account) and a liveness bug (money can leak if the spec isn't declared fair).
The demo works really,
really well. Almost everyone went straight from "who cares?" to "holy crap". People immediately start talking about problems they had at work and asking how TLA+ can help them with that. And it's not just conventional software engineers: I got questions about devops and deployments, data ETLs, security, workflow validation, etc. It's really amazing how
excited people get once they see it actually run.
(Not that telling was entirely ineffective. Jay Parlar and I hosted a formal methods open sessions that got around 30 people. Everybody seemed to really enjoy that; Jay is much better at explaining w/o demos than I am.)
When it comes to persuading people to try TLA+, what's worked for you?