Quoting from Bit Torrent founder (Bram):
"The utility of formal methods for practical code writing is an interenting debate. As you might expect, I have some thoughts on the matter.
Code winds up much better if it is rewritten pragrmatically with experience. I think there isn't a single line of BitTorrent which hasn't been rewritten at least twice. If I had been using formal methods, the whole program would essentially have been proven once for each rewrite. Much easier is to write the whole program once using more direct methods and then audit it."
Write the program and then audit it? I thought unit testing happened first? Hmm.. sounds like someone doesn't even know about how unit testing is supposed to be practiced... If you read up on any of the unit testing methods from the founders themselves, they imply you write the tests before you write the code (I think this is pretty stupid, but that's what the unit testers say you should do if you actually read their material).
(Jokingly, maybe some unit tests would help correct "pragrmatically" and "interenting". Or maybe, you could use a strongly typed formal spell checker)
"The much-vaunted slow programming of the space shuttle is mostly a triumph of beurocracy. Switching from a B&D to a write-then-audit methodology would drastically reduce costs and result in better code."
Huh? Write and then audit? I thought unit testing was about auditing before you write. Contradicting ourselves here aren't we now. I guess Bram doesn't know what unit testing is, according to the experts who developed it, and recommended you start writing tests first, not after.
If he knew anything about unit testing and had done any research on it, you are supposed to write your tests first, not after... Read some heavy hitters on the subject, the founders of unit testing.. and you will see.
"While I'm still not convinced of the practical utility of formal methods, I'm completely sold on unit tests."
Not convinced of math, either, then? Math can't be practical? Not convinced of formal spell checkers, formal type systems (integer vs byte vs string vs boolean),
Formal methods can be combined with testing, anyway. You don't have to pick one or the other - as Bram (Bit Torrent founder) makes it sound. Taking one apple and proving that adding another apple will equal two apples - is a test. Many formal mathematicians fill in values and test their theories. The idea that formal folks don't use testing and the idea that unit testing is completely separate from formal method is nonsense.
An interesting book on the subject is "The Science of Computing: Shaping a Discipline" which discusses the ongoing flamewar of formal verification vs testing that is a debate over 50 years old.
In math, people can fill in values and test equations out. But that's hardly the important part of math. Anyone can test out some apple addition. In software you can never provide enough tests to even begin to cover the program. There are always more and more tests that will never be written (but the religious unit tester advocates don't admit this, they actually are dumb enough to believe a certain amount of tests covers a lot, when in fact tests cover almost nothing). Refer to the chess board example from Dijkstra. Thinking you can write a few unit tests for each little unit is suicide - testing will never be finished, ever. Refer to the chess example from Dijkstra in the article On the Cruelty of Really Teaching Programming
http://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1036.html
You might be thinking that Dijkstra is some old dead grump and we shan't listen to him. However, the chess board example is real. It is a real example. It is brilliant and easy to understand. Read the article. Think about testing all the checkerboard squares and what a waste of time it would be. Think of how complex a software program is compared to a checkerboard, and how many more tests would have to be written to cover the software checkerboard. See why writing more and more unit tests can be stupid and dumbfounded.
Unit tests are actually more of a bug reporting activity.. not a proving or specification activity! They can show presence of bugs. They are good for that.
Showing formally that a program is correct, and doing (incomplete) tests are both useful ways to make programs better. Believing that testing and formal methods are magically two different political parties are similar arguments to:
- Art is right and Science is wrong - paint doesn't involve any science
- God is correct, Science is wrong.. science is too formal, God is nicer.
- Rock musicians are right, Classical music is wrong
The problem with unit testing advocates is they act like rebels and deny any sort of form is good. They want to be bad boys and go against everything that has form. Math is wrong, art is right. Has to be. God is right, science is wrong. Science is too formal - God is more creative. Let's take sides and side with art, and god. Screw science. Screw math. They are too formal.
A unit test is a test which exercises some code without requiring the rest of the program be linked in. The approach to writing them is to make them all pass/fail, and have a script which runs all unit tests and reports failures. Whenever a unit test is failing, fixing it becomes the top priority. Anyone whe doesn't fix their unit test breakage with the excuse that getting all the tests to pass is impractical anyway should be fired, (or at least, have their commit access revoked).
While formal methods clearly slow down development, unit testing actually speeds it up by reducing debugging time, making it not only practical but easily justifiable.
Is he really just throwing up straw men now? Unit testing slows down development since people spend a lot of time writing millions of unit tests that will never cover the entire program, you nimrod. Formal methods slow down development because people spend time writing proofs and specifications. However unit tests are never and can never be finished. Unit testers think that you can write a certain amount of tests and that covers it. Programs require millions of tests, not a few! You can never finish testing - there are an infinite amount of tests to perform. People that write unit tests do not write all the tests, for if they did they would not finish their program until thousands of years later, if at all. Both testing and specifying integrity takes time, and both are useful.
Writing good unit tests is more art than science. The general idea is to try to make the unit test code simpler than the code it's testing, and also to make the test code assert statements from a fundamentally different perspective than the code itself. Formal methods, by contrast, wind up repeating the code a lot, and thus aren't good at catching specification bugs.
Formal methods aren't good for catching specification bugs? Like how type systems and database integrity checks don't help us? Sure, sure.
Footnotes:
When I use the term nimrod, I am joking. Recently, I was informed by C2 Wiki members that they need special pointers and little helpers (as in, can you wipe my bum for me) to point out where I am being funny, and where I am being serious. Well, mimrod is not a serious word. Rather I mean it figuratively, like "a moron" or "an idiot". Seriously I'm joking, serious. Joking. Serious.
Also, when I use phrases like "screw science", I am being ironic and sarcastic. I personally don't think science should be screwed, it is the unit test religious advocates who think science and math is a waste of time. Did you know engineers use science, theory and math, by the way - oh unit testers?
Explaining my jokes, however, does not make it funny; and explaining my jokes does insult the intelligent reader who already got it.
|
