Proving vs Testing

How do you know that your code works? I imagine most developers would answer that they know their code works because it's been tested by either them, QA, users, or some combination of those actors. In his book Clean Architecture, Uncle Bob calls this the scientific approach to software development. This is because code, like a scientific claim, is falsifiable: You can run tests to show it does not work.

Not everyone, however, agrees with this approach. Edsger Dijkstra, a towering figure in the history of computer science, argued that a test can only show that a piece of code does not have a particular bug. Tests do not prove that your software works. In his mind, you have to use math.

So, why don't we use math to prove that our software works? Why do we hear about practices like Test Driven Development (TDD), but not Math Driven Development? I speculate that the answer involves a number of factors. One is that even if you prove something mathematically, you still have to translate it into code; that translation creates the risk of introducing bugs and negating the whole endeavor. Another factor is that this approach may require a significant upfront investment.

Perhaps the biggest reason why Dijkstra's approach didn't gain wide adoption is because not all software requires it. There is a wide spectrum of applications that even when a bit buggy are still very useful. For instance, I just used a graphics editor. It threw an error when I tried to draw a math function. That program has at least that one bug. But it is still very useful.

What about the cases where you need more confidence in your code? For example, what if you are a designing a distributed system to host files for millions of users? The engineers at Amazon behind implementation of AWS utilized an approach that is closer to Dijkstra's vision. They used a specification language. In particular, they used TLA+.