Building a complex distributed system? How do you verify your design doesn’t have issues with consistency, performance or fault tolerance?
Amazon has been using formal methods to verify its distributed systems since 2012. Now, major players like Amazon, Microsoft, MongoDB, Confluent, Oracle, Elastic, CockroachDB, and many more are all embracing formal methods for their systems. Despite the immense benefits and relevance of this technique in modern software development, its widespread adoption has been hindered by the complexity of existing tools.
In March 2023, Andrew Helwer wrote a thought-provoking article comparing Python with PlusCal & TLA+, while implementing a 45-year-old algorithm.
Reflecting on his insights, I find myself resonating with much of what he shared. Indeed, when it comes to publishing algorithms, opting for an executable language over arbitrary pseudocode stands out as a superior choice.
A quick recap from his article:
Python made a very compelling case for itself here. The final algorithm, naive algorithm, and property-based testing code combined took up only 35 very readable lines!
