Awesome Knuth Quote On Code Proofs

My friend (and former boss and business partner) Micah found this gem of a quote from Donald Knuth addressing code proofs.

Beware of bugs in the above code; I have only proved it correct, not tried it.

Micah writes more on the topic and reminds me of why I enjoyed working with him so much. He’s always been quite thoughtful in his approach to problems. And I’m not just saying that because he agrees with me. ;)

On another note, several commenters pointed out that one thing I didn’t mention before, but should have, is that verifying the quality of code is only one small aspect of unit testing and Test Driven Development.

The more important factor is that TDD is a design process. Employing TDD is one (not the only one, but I think it is a good one) approach for improving the design of code and especially the usability of your code. By usability, I mean from another developer’s perspective.

If I have to create twenty different objects in order to call a method on your class, your class is probably not very usable to other developers. TDD is one approach that forces you to find that out sooner, rather than later.

A code proof won’t necessarily find that “flaw” because it is not a flaw in logic.

Comments

6 responses

Evan • November 29th, 2007
Not to mention that test hooks make awesome extensibility hooks..
Evan

Micah • November 29th, 2007
I suppose I should start disagreeing with you more before people think I'm your infrequently-posting-alter-ego...

Frans Bouma • November 29th, 2007
Let's counter this with Micah's logic.
Say I have a Linq provider, which should be able to parse an unlimited number of different expression trees to SQL.
How do you know when that code is ready to be shipped to customers?
That's a fair question I think, and given the massive scope of the code, it's not really a simple one either I think.
I agree what Micah said about provability in science, but that's nothing new, as what he said is simply the cornerstone science is build on: something is true if there's not a prove possible which proves it's not true. So all you need is a simple unittest to prove code is broken, completely agreed with that.
The flipside of that is that when they all turn up green, you haven't answered your question about "Am I done? Is this shippable?".
I now work for 2.5 months on our Linq provider and if there's one thing where unittests are pretty meaningless other than to see if there is at least ONE situation where the code works, it's with code like a Linq provider.
Take this query:
var q = from c in nw.Customers
where c.Orders.Count(o=>o.Employee.Country=="USA") > 10
select c;
compare it with:
var q = from c in nw.Customers
where c.Orders.Where(o=>o.Employee.Country==USA").Count() > 10
select c;
They result in the same resultset. Yet, the expression trees are completely different w.r.t. 'Count'.
Add to the mix a query where Count is used in group by statements where Count() has to be swapped in place in the tree, and you're in for a lot of fun :). I.o.w.: the number of different trees to expect with Count and how to threat Count is already big, left alone the set of tests to cover them all. So that's not going to work.
Honestly: answer for me the question I asked in the first sentences of my post. Saying on a weblog that unittests are great etc. is OK, nothing against tests, but with real-life problems like the one I described above, does what you say really solve that real-life problem?
Oh, before you ask, no I don't have a gut-feeling-o-meter which tells me 'this should be OK'.

orcmid • November 30th, 2007
The Kindly Programmer explains the origin of the quote in the last entry on his FAQ page: http://www-cs-faculty.stanf...

Micah Dylan • December 6th, 2007
Science and software

Hakon • December 9th, 2007
You see a lot more of quotations about software development on my site: www.SoftwareQuotes.com - quotations from the world of programming.