Page 2 - Testing; the key to heaven or hell?

Formal proofs are not a substitute for good unit testing.
Firstly only a small subset of what you write will be amenable to any sort of formal proof.

Secondly you can only prove that an algorithm is correct, not your implementation of it. You may have made a typo, accidentally used the wrong variable, or anything like that. You will only find this out by running the code and checking the result.

Thirdly, even if the algorithm is correct there is no defense against someone else changing it later, perhaps as requirements change. many teams do not practice code ownership, so anyone can come along later and change "your" code. How will they know that your formal proof no longer applies to their change?

You get insights into your code from working through a formal proof. I get insights into my code by writing a test for it before I write the code to make the test pass.


I run the tests before, during and after any change - that is a core practice of TDD. It gives me the freedom to make sure my code is both well crafted and correct.

You make it sound like writing the tests is a huge overhead. It is not - before I started doing TDD I spent far longer tracking down problems with the debugger or trawling through log files than I now spend writing tests.

Dave

Quite right. And unit tests are not a substitute for formal proofs.

This depends very much on the distance between your programming language, it's implementation and the laws of mathematics and, generally, the support your environment has for automatic forms of "safety". You *can* prove important properties of code and the world of formally provable systems exist because of this. Compile-time checks imply a limited sort of proof. Pre and Post conditions in Eiffel or Ada imply a type of proof that doesn't depend on testing. Functional languages can go much further with it. This is important because sometimes it's necessary to prove that conditions apply under all possible circumstances not just under the unit tests a programmer happened to write, which satisfied him that "it's working". When Knuth said "Beware of bugs in the above code; I have only proved it correct, not tried it.'' he was talking about implementing algorithms in assembly language.

Having said that, I use unit testing every day and never write formal proofs for my (far from safety-critical!) code.

Perhaps I am missing something here, but I would like to suggest it might be that the nature of the work being done influences the value of creating formal proofs. If you are devising compression or sorting algorithms, for example, then you are probably going to find some program or methods of proof theory applicable. I don't work in that area, however. My work consists almost entirely of what is typically called enterprise software development. I use sorting algorithms, but I don't invent them; I use financial formulas but I don't devise them - that is done by financial experts; and so on. When I use these things, the results have to be as expected, but they typically will be as expected as long as I didn't make mistakes, and my unit tests usually expose my mistakes. I have not found any useful application of formal proofs in my work, which is not to say that such a use doesn't exist - I just haven't found any case where it would be helpful to me.

It is useful to me to understand as much about the functionality being developed, but the process of developing generally includes a great deal of discovery about the actual requirements that were not, or could not be discovered by the people supplying the formal requirements. This is where IID and Agile practices have been useful to me. It becomes a collaborative effort to come to a successful result. (Note that among these practices is TDD). What I am saying is that it is not uncommon for me (the developer) to be the driving force behind the solidification of the requirements (which traditionally are meant to be done "up front" - but which are almost always sketchy, at best, "up front"). Using Agile practices, it is at about the time the development is done that the requirements are more or less understood.

Perhaps someone reading this has had experience applying formal proofs in this scenario. It would be interesting to hear of any experiences and especially successes.