Confidence through proof

This week marked the inauguration of Q.E.D. Hour. This is a weekly lunch hour where we talk about techniques for writing provably correct software. The goal of Q.E.D. Hour is to gain confidence in our code.

ConfidenceThere are several ways to build confidence in your code. You can write specifications to record what the user wants or how you intend to build it. You can single-step through it in the debugger. Or you can write unit tests.

The problem with all of these confidence builders is that they can only give you confidence in the situations that you've thought about. They can't tell you anything about the situations that you haven't considered.

What if the user does something not in the use case or user story? Do you write another use case to cover that scenario? When does it stop? Can you ever write enough use cases?

You can see what the code is doing when you single-step through it in the debugger, but what would it do if you passed in different parameters? Can you every do enough debugging?

You can see that every unit test you've written passes. What about the unit tests you haven't written? How do you know that the code is correct for all situations? Can you ever write enough tests?

Even 100% code coverage doesn't save you. The line that references "Customer.Name" is covered by tests, but what happens when Customer is null?

Mathematical proof is the only way to know that code is correct under all possible conditions. All of the other techniques are empirical. They only verify the code in one situation. Proof, on the other hand, is deductive. It verifies code for an entire class of situations.

Both empirical and deductive confidence builders are required. Without empirical evidence, you can't be sure that you wrote the code correctly. But without deductive proof, you can't be sure that you wrote the correct code.

Leave a Reply

You must be logged in to post a comment.