October 27th, 2006, 06:33 AM

Originally Posted by netytan
If you’ve done any formal training then you should remember learning about proving theorems, usually in some discrete mathematics or algorithms course. Generations of study in mathematics have shown that this is
the reliable way to prove if things like this work as intended!
Testing against a limited number of cases just doesn’t square up to that, but it is easier.
For the most part I’d rather spend the extra time to produce a semiformal proof, than write up (and maintain) dozens of tests. The results tend to be far better in my opinion because I inevitably get some new insight into the problem domain by doing this.
...
I can’t say that I commonly work with dozens of people, but any wellwritten code should be resistant to this kind of work. If you make good use of abstraction and high cohesion, then no matter how much you change how your code works you can’t break anyone else’s work – Think encapsulation on a massive scale
.
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.
If the code is badly crafted then sure, make sure that you run your tests after every change!
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
Comments on this post
October 30th, 2006, 10:54 AM

Originally Posted by DevCoach
Formal proofs are not a substitute for good unit testing.
Quite right. And unit tests are not a substitute for formal proofs.
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.
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. Compiletime 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 safetycritical!) code.
October 30th, 2006, 05:38 PM

Originally Posted by jamieB
Quite right. And unit tests are not a substitute for formal proofs. etc...
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.
Last edited by woodyz; November 15th, 2006 at 11:36 AM.