One thing I've never really seen discussed is proving unit test coverage. Taking the clojure example above and its unit tests, nowhere does it make any attempt to show that the few test cases chosen provide a complete coverage of all possible bowling scores. Without that what have you really shown? Sure I can look at it and my gut feeling is, yea that should be enough, but I got that from looking at the OCaml code as well
In the blog post Brad Fitzpatrick is quoted as saying "Write a test. Prove it to me." Now maybe it's my maths background, but when someone say "prove it" a expect proof, and the bowling unit test example proves nothing more than that it works in a few common cases.
Yes I realize that proving anything non trivial in programming is Very Hard, but without any sort of reasonable attempt and even talking about this problem TDD seems more or less ad hoc to me.
I can't "prove" my code, but I can prove that my test executes every function, every line and takes every branch and every return. I run my test using valgrind (callgrind with a few options), then I wrote a valgrind parser and combined that with a c++ parser and output the results. Some fun tidbits:
Every time I discovered that a bit of code can never be executed.
The amount of functions that I never even call, even when I am using my test generator (built on top of the same c++ parser)
I enjoy coding. If I spent 1 hour coding a test that finds nearly all of the bugs in a class that means later I wont spent a week deciphering reports and fixing bugs that are annoying users. I get to hack more and my users get more stable code.
You should have a look at QuickCheck. It's a Haskell library where you (more or less) specify laws that your program should satisfy, and it generates test cases on its own. I found it very useful.
Proving test coverage is just as (in)feasible as proving correctness. This is the elephant in the room for testing: it relies on programmer intuition to enumerate cases. It's easy to neglect a case both in the implementation and in the test. This is why tests are better at finding regressions than new bugs.
In the blog post Brad Fitzpatrick is quoted as saying "Write a test. Prove it to me." Now maybe it's my maths background, but when someone say "prove it" a expect proof, and the bowling unit test example proves nothing more than that it works in a few common cases.
Yes I realize that proving anything non trivial in programming is Very Hard, but without any sort of reasonable attempt and even talking about this problem TDD seems more or less ad hoc to me.