Writing correct code in software engineering is a complex and expensive task, and too often our written code produces inaccurate or unexpected results. There are several ways to deal with this problem.
In practice, the most common approach is to write tests, which means that you are writing more code to test your original code. However, these tests can only detect problems in specific cases. As Edsger Dijkstra noted, “testing shows the presence, not the absence of bugs.”
A less common approach is to find a proof of correctness for your code. A software proof of correctness is a logical proof that the software is functioning according to given specifications. With valid proofs, you can cover all possible cases and be more confident that the code does exactly what it was intended to do.