What a mathematical puzzle can tell us about verifying software safety

In software, you can find bugs when you do traditional testing. However, you can never prove their absence. You test a few cases, deploy your code, and hope for the best. For everyday apps, maybe that's fine. But what about the software controlling airplanes, medical devices, or nuclear power plants? One bug could be catastrophic.

This is where the term 'formal verification' comes into play. Formal verification is an approach where mathematical proofs are used to guarantee software correctness. Instead of running test cases, we write logical specifications of what our program should do, then mathematically prove that it meets those requirements - for every possible input, every possible state.

As a simple hands-on example we will be using the puzzle 'Tower of Hanoi' to explore what a mathematical proof looks like and how we actually use them to verify software correctness.

(Photo: Shutterstock)