This is why I’ve become such a vocal advocate for formal methods like TLA+ over the last few years, and why I’ve been working on model-based testing this year. These tools are all about finding those edge cases and preventing them before they can happen in production.

https://twitter.com/definekuujo/status/1572114691585089536

When arguing that edge cases matter, I’ve sometimes used visualizations of TLA+ model behaviors to demonstrate failure scenarios that can happen in distributed systems. Rather than argue my concerns, it can be more effective to point to the math that proves they are relevant.

This is exactly the right question to ask. I’ve been talking about this with a few people lately. I actually think it goes both ways. There are two challenges: ensuring the spec specifies a practical implementation, and ensuring the code correctly implements the spec. (1/?)

https://twitter.com/lemmster/status/1227716019264733189

This was the first spec I’ve written that really encountered the first challenge. I initially modeled some operations in a single step that in the implementation would have been problematic as it would have required a mutex around a database (consensus) call.