The best question asked this week: What, exactly, are you trying to prove?
To prove the correctness of code, you need to know exactly what correct behavior is for the code, i.e. a complete and unambiguous specification for what the code should do. So tell me dear reader, when was the last time you received an unambiguous fully detailed specification of an application?
If I ever received such a thing, I would simply execute that sucker, because the only unambiguous complete spec for what an application does is code. Even then, you have to ask, how do you prove that the specification does what the customers want?
Proving that the software meets the rigorous specification written by the customer before they had seen the software work, before they had tried it, has been of secondary importance to me in my career. The overarching concern has been the transformation of the requirements from what the customer guessed
they might need, based on superficial desires and buzzwords, into what the customer discovered
was actually important, over the lifetime of the project.
No, no, no! You don’t know what you want!
Hey, I am not blaming customers. They don’t know what they want because nobody
really knows what the optimum finished software looks like before development begins. Not the Customer, not the Developers, and not even the “Architects,” “Product Managers,” “Business Analysts” or anybody else who think they are a requirements expert.
Software development is a process of discovery, for the customer, for management, and for development. As information is acquired—through inquiry, inspection, or experience gained from misadventure—our understanding of what we are trying to accomplish is refined. In that respect, every tool, be it a programming language, a development process, or a testing practice, must be judged for its contribution to the transformation
of both the requirements and the software over time.
I am not saying that strong typing
or provability, iterative development
or BDD, or anything else is necessarily better or worse in this respect. I am just pointing out that the surface, buzzwords for these things—fewer bugs, provability, test coverage, separation of concerns—are not the goal, they are ways and means of achieving the goal, which is the discovery of the true requirements and the delivery of working software which meets the true requirements over the project’s complete span.