Program correctness. It’s important and certainly worth study. Formal verification is very worthy, but perhaps a bit deep for my taste. Though I am fascinated with languages that are mathematically sound. Not only does it sound good, but it feels good too.
Work has presented me with opportunity to re-visit some code that I wrote more than a year ago. Were I to program today what I programmed a year ago, it would look very different. I think that’s a good thing, as it means that I’m learning and growing. But it also brings to mind a question of correctness. The code is correct, it meets the business requirements, but it could be more correct in that it could have been written more efficiently.
A different situation at work is allowing me to think about a set of business rules that a colleague and I have been working on now for the past eight months or so. As we’ve worked on this unit of logic our views about the problem and what is ‘correct’ have changed significantly. At times we’ve made changes to our algorithms. Other times we’ve approached the business rules philosophically by re-defining the task we’re trying to accomplish. Interestingly enough though we change algorithms and/or re-define tasks, in the eyes of the customer the meta-rules remain the same. However from the perspective of verification, I believe that we’ve created a moving target. Though the meta-rules remain the same, there have been many changes (some small, some not so) which should get us to the same set of meta-results. I suppose the question is this. In an environment were change is the constant, what is the best way to verify program correctness? Or to ask the same question with different words. When making constant changes/re-definitions to the nuts and bolts, how is the consistency of the meta-rules to be maintained and verified?
One might argue that this is where unit tests will come to my aid. However, I’m still having trouble buying into unit tests for database driven business processes. When the database is removed (as most unit testers say is prudent) many of the most critical parts of our application are cut out of the picture. I’m not so concerned about presentation logic, but I’m absolutely paranoid about getting the right data out of the database in the most efficient manner possible.
I’m intrigued by this ‘moving target’. It’s more like research. What we thought to be correct eight months ago isn’t so correct today. Like the code that I wrote over a year ago, it’s encouraging to be able to look back and note that there are things that I would do differently with today’s knowledge. I’m comfortable with change, and with change comes the need to verify that the results are still good. Verification is the part I’m still uneasy about. It’s the weak link. I don't know what the answer is, but I’d like to believe that I’ll be able to recognize it when it is presented.