Dijkstra was right though. We have credit card thefts, SCADA systems run amuck (Iran's nuclear centrifuges for example) and serious risk to life and limb as a result.
The thing is, we can't measure how much better off society would have been had we baked those rigorous methods into the base of our tools. Or the benefit in increased velocity if we didn't have to come back and fix stupid defects later.
Further, with TDD, BDD, unit tests, etc we're slowly moving towards the world Dijkstra argued for in the first place. Dijkstra could see the Forrest while industry was bedazzled by the trees.
If you want proof, you will always agree with Dijkstra ;-) Unfortunately, I can't summon an alternative universe where Dijkstra got his way. However, I can say that Dijkstra is rolling over in his grave if he heard you compare testing to his approach. To him, empirical approaches were appropriate for the physical world, where items vary, materials deteriorate, and operating conditions are unpredictable. In the digital world, where systems are vastly more complex but made out of ideal, eternal elements, the proper tool is not empiricism, but mathematics. That is Dijkstra's message: mathematics is the right tool for programming, and we are making a costly error by applying empirical engineering methods instead.
Testing is just another messy empirical approach to a mathematical system. The master would be appalled.
I would think that unit tests have nothing to do with Dijsktra's notion of verification. I even seem to recall he had a horror of software testing. If you can prove something, why test it?
I recently read the free Kindle chapter of David Gries' book The Science of Programming, recommended at a previous discussion of this essay:
http://news.ycombinator.com/item?id=1667081
My impression of his thesis so far: unit tests are great, but the challenge is figuring out exactly what unit tests you need to write. Formal methods give you a way of doing that.
Comments
Dijkstra was right though. We have credit card thefts, SCADA systems run amuck (Iran's nuclear centrifuges for example) and serious risk to life and limb as a result.
The thing is, we can't measure how much better off society would have been had we baked those rigorous methods into the base of our tools. Or the benefit in increased velocity if we didn't have to come back and fix stupid defects later.
Further, with TDD, BDD, unit tests, etc we're slowly moving towards the world Dijkstra argued for in the first place. Dijkstra could see the Forrest while industry was bedazzled by the trees.
In short, you claim we have it better. Prove it.
If you want proof, you will always agree with Dijkstra ;-) Unfortunately, I can't summon an alternative universe where Dijkstra got his way. However, I can say that Dijkstra is rolling over in his grave if he heard you compare testing to his approach. To him, empirical approaches were appropriate for the physical world, where items vary, materials deteriorate, and operating conditions are unpredictable. In the digital world, where systems are vastly more complex but made out of ideal, eternal elements, the proper tool is not empiricism, but mathematics. That is Dijkstra's message: mathematics is the right tool for programming, and we are making a costly error by applying empirical engineering methods instead.
Testing is just another messy empirical approach to a mathematical system. The master would be appalled.
I would think that unit tests have nothing to do with Dijsktra's notion of verification. I even seem to recall he had a horror of software testing. If you can prove something, why test it?
I recently read the free Kindle chapter of David Gries' book The Science of Programming, recommended at a previous discussion of this essay: http://news.ycombinator.com/item?id=1667081
My impression of his thesis so far: unit tests are great, but the challenge is figuring out exactly what unit tests you need to write. Formal methods give you a way of doing that.
His opinion on tests: they can only show the presence of bugs, not their absence.
That statement means: "they can only show the presence of 0 or more bugs, not the absence of any bugs". That's not just his opinion: that's a fact.