Hi Elliott,
Thanks for posting your experience.
- I actually spent the majority of my time understanding the protocol (i.e. tracking down and talking to the authors, reading design docs, reading code); the process of writing PlusCal went really quickly and smoothly.
Yes, people are so used to starting to think only when they start writing code, that they don't realize that the hard part of programming is the thinking, not the coding. And they write bad code because thinking in terms of code leads to bad thinking. Since specifications are so much smaller than programs, it's harder to make that mistake--especially when the spec language is expressive enough to make it easy to express your ideas in the language.
- The model checker did find an issue, but it was already a known and tracked issue (something can go wrong if a writer takes a really long time to commit a database transaction while the cache is being restarted).
Did you know about that issue before you wrote your spec? If not, that's a very good illustration of the usefulness of specs even if the problem had already been discovered.
- I had to keep the model's parameters really small, or face a tremendous combinatorial explosion of states (though I'm not ruling out the possibility that I could've formulated the spec in a different way that's more conducive to model checking).
As this may have led you to realize, even tiny models can be very effective at finding bugs.
Cheers,
Leslie