Was My Code Provability Post An Inspiration To Joel?

Dec 4, 2007 code tdd methodologies suggest edit

Note that in the same vein as Pele, Ronaldinho and Ronaldo, Joel has reach that Brazillian Soccer player level of stardom in the geek community and can pretty much go by just his first name. Admit it, you knew who I was referring to in the title. Admit it!

Please indulge me in a brief moment of hubris.

I was reading part 1 of Joel Spolsky’s talk at Yale that he gave on November 28 and came upon this quote on code provability…

The problem, here, is very fundamental. In order to mechanically prove that a program corresponds to some spec, the spec itself needs to be extremely detailed. In fact the spec has to define everything about the program, otherwise, nothing can be proven automatically and mechanically. Now, if the spec does define everything about how the program is going to behave, then, lo and behold, it contains all the information necessary to generate the program!

Hey, that sounds familiar! By coincidence, I wrote the following on November 16^th^,12 days prior to Joel’s talk…

The key here is that the postulate is an unambiguous specification of a truth you wish to prove. To prove the correctness of code, you need to know exactly what correct behavior is for the code, i.e. a complete and unambiguous specification for what the code should do. So tell me dear reader, when was the last time you received an unambiguous fully detailed specification of an application?

If I ever received such a thing, I would simply execute that sucker…

Sure, it isn’t exactly an original thought, but the timing seemed too coincidental. Could it really be? Could my post inspired one small point in a talk given by someone of his stature?

For a moment, I allowed myself to dream like a true fanboy that Mr. Joel really did read my blog. Until I read this (cue sound of pots and pans crashing down)…

The geeks want to solve the problem automatically, using software. They propose things like unit tests, test driven development, automated testing, dynamic logic and other ways to “prove” that a program is bug-free.

Crestfallen, I realized Mr. Joel indeed did not read my post, in which I claimed…

Certainly no major TDD proponent has ever stated that testing provides proof that your code is correct. That would be outlandish.

To be fair, I wouldn’t call Joel a major TDD proponent, but I hoped he would understand that TDD is about improving the design of code and also providing confidence to make changes to the system. It’s no proof of correctness, but can be a proof of incorrectness when a test fails.

Oh well, one can dream.

Found a typo or mistake in the post? suggest edit

Comments

21 responses

Haacked • December 3rd, 2007
I should mention that the talk is still a very good read. Joel is quite the gifted writer.
commenter • December 3rd, 2007
Hmmm. Surely it's possible to completely spec out what a function will return without expressing it as an executable algorithm. In this case, you wouldn't be able to just execute the spec.
Chad • December 3rd, 2007
@commenter
If you are defining the spec down to the function level you have already lost the battle.
And, yes, if you completely spec what the function will return (and what it will NOT return) you will have basically written that function.
Anydiem • December 3rd, 2007
I miss the old Joel. A lot of the older content on his site is great, and I love his writing style, but lately it's become the FogBugz Marketing Blog. When there is content, it's often something I can't get behind, like the one where he stated his need to develop his own language and compiler, or this one.
The theory that automated testing is without merit because it can't prove a GUI is usable or that code is flawless, doesn't really make sense to me.
I would post this in Joel's comments, but he doesn't want to hear from the readers, so I posted it here since your reaction was similar to mine.
pat@veloc-no-spam-porfavor-it. • December 3rd, 2007
Has Joel looked into .NET yet, or does he still consider it 'cover fire' from MS? (How about frameworks in general?) I am now re-connected with the blogosphere (subscribing to around 50 blogs now), but Joel's is not one of them this time around. Doesn't sound like I'm missing out on much based on Anydiem's comment. Am I wrong?
John Radke • December 3rd, 2007
Well...if unit testing doesn't prove correctness, what DOES it do?
Anydiem • December 3rd, 2007
@John Radke
It doesn't prove that your code is absolutely correct. It proves that given a particular input that it will produce a particular output. It's not a silver bullet that makes code perfect. It's a design tool that helps to remove fear that changing code will break its functionality.
Haacked • December 3rd, 2007
@John Radke I'm glad you asked. I wrote about it in this post. That post references another post worth reading.
Haacked • December 3rd, 2007
@Pat Good to see you blogging, man! Yeah, I think overall Joel is still worth reading. If nothing for the excitement to see what inflammatory thing he says.
Seriously though, the guy is crazy smart and has good things to say. The fact that he's opinionated is a good thing. It's good to check your own assumptions sometimes. So while I think he's wrong on some things, he forces me to think hard about why I think he's wrong.
At the same time, he's right about a lot more things.
Jeff Atwood • December 4th, 2007
Interesting that Joel explicitly mentions "80 percent" of programmers in that talk on Nov. 28.. this post is dated Nov. 25:
http://www.codinghorror.com...
Ryan Smith • December 4th, 2007
I still think that Joel is fun to read, but the bigger problem is that he hasn't written any decent length articles in a while.
A lot of his site has become a marketing blog for FogBugz, but at least he still tries to relate it back to improving software development practices.
I guess his lack of posting give me more time to read things like Haacked and Coding Horror.
Jeff Handley • December 4th, 2007
When I read Joel's post, I too thought maybe he was referring to you! But I also got the impression later on that it was just a coincidence.
I do like something you said here though... "It’s no proof of correctness, but can be a proof of incorrectness when a test fails." That is an excellent statement!
I am not a TDD advocate, but I see its benefits. Sadly, I've talked to many people and heard and read from a lot of people who seem to think TDD does prove correctness. But, as you've said here, it doesn't. It can only make you aware of failures against scenarios that are expected to succeed.
Tom • December 4th, 2007
Haack, you're the Diego Maradona of programming.
I don't even bother reading "the Joel" anymore. Real developers don't write 70% of their blogs about traveling.
Haacked • December 4th, 2007
@Tom Who told you about my coke habit? I kid! I kid! I'd rather be the Kaka of programming these days. That kid is having quite the year. He'll be FIFA player of the year, no doubt.
commenter • December 4th, 2007
"If you are defining the spec down to the function level you have already lost the battle."
Why are arrogant programmers so keen on this kind of irrelevant nit picking?

"And, yes, if you completely spec what the function will return (and what it will NOT return) you will have basically written that function."
So if I write 'this function will take a public key and calculate the corresponding private key in <1 second on yer average PC', I've 'basically written the function'?
Obviously I've missed the language that'll implement that for me - sounds like a real silver bullet for productivity.
The point is that you could exhaustively spec out the behaviour you wanted from a program and:
1) It might even be impossible to implement.
2) There wouldn't necessarily be a way to automatically transform that spec into executable code (unless you count having humans write the code as being an automated process)
I await your glib, point-missing response. :)
Denny Ferrassoli • December 4th, 2007
Certainly no major TDD proponent has ever stated that testing provides proof that your code is correct. That would be outlandish.

I'm still wrapping my head around TDD but I think the proof that it gives you is that: Given X, Y must be true. Where X is your input and Y is your output. I can't prove that my code is correct but I can prove that my result is correct when X = 1. I don't think that TDD proves code correctness, it proves result correctness.
Haacked • December 4th, 2007
Interesting point. However, the main topic is code provability, which requires two things: 1. A spec. 2. A code to prove against that spec.
If the code to meet the spec is impossible to write the code, then you have nothing to prove. ;)
So let's use a little common sense here. When we say "all specs", we're really talking about the set of specs in which the code is possible to write to meet that spec.
As Joel says in his post:

To use terminology from information theory: the spec needs just as many bits of Shannon entropy as the computer program itself would have. Each bit of entropy is a decision taken by the spec-writer or the programmer.
David Seruyange • December 5th, 2007
To: Joel Spolsky
Date: July 26, 2005
Re: In House Developers
https://haacked.com/archive/...
Haacked • December 5th, 2007
@David at least this time, he focuses on the conditions for in-house devs rather than the quality of the devs themselves.
Scruffy-Looking Cat Herder • December 13th, 2007
Dependency Injection House Call
Alyosha • December 19th, 2007
If you look at the JoelOnSoftware archives you can find references to "a fully detailed spec is the code" subject mentioned above. Joel's talk mainly covered subjects he already wrote about.