He makes this observation:
[...]]the idea of immediate compilation and "unit tests" appeals to me only rarely, when I’m feeling my way in a totally unknown environment and need feedback about what works and what doesn’t. Otherwise, lots of time is wasted on activities that I simply never need to perform or even think about. Nothing needs to be "mocked up."I believe him. I also draw a few inferences.
One is that Knuth probably doesn't spend much time working on systems that do their work by intimately coördinating (with) six or eight other systems with very different usage patterns, metaphors, implementation stacks, space and time complexities, latencies, interface styles/languages/protocols etc. etc. etc.
Another is that he probably doesn't spend much time working on problems that are incompletely and ambiguously described (and that can't be fixed in a meaningful time and/or budget), part of an ad–hoc domain, intrinsically fuzzy, aiming or a moving target from a moving platform, subject to capricious and arbitrary constraints, etc. etc. etc.
And thus is the working life of the research computer scientist different from the working life of the commercial software engineer. I'm tempted to say (and so I will) that the jobbing industrial programmer spends more time in an unknown environment and needs more feedback (and, right now!) about what works and what doesn’t more often than a researcher does.
17 comments:
It is difficult (and therefore an interesting research problem) to make it easy for people who fit #1 to do #2. But where is that research happening? For some reason, the fields of HCI and formal methods rarely interact.
: subject to capricious and arbitrary constraints, etc. etc. etc.
Those are called "users", I believe.
To follow up on what Nat said: the low hanging fruit for formal verification lies in static type systems. It is a very active area of research to try to make type systems that are both capable of proving more interesting things and easy to use. Unfortunately, mainstream languages are stuck with type systems that either don't prove much of anything interesting or are hard to use or both. Is it any wonder that dynamic typing and extensive unit testing are seen as better answers by so many?
@jhi I was thinking more of "managers", but "users" works too.
@James, I won't argue about the absence of type systems that are both useful and usable.
Increasingly these days I wonder if what folks are finding is that dynamic typing and extensive unit testing give very strong validation, which maybe trumps formal (or any other sort of) verification.
Beware of bugs in the above code; I have only proved it correct, not tried it. - Donald Knuth (look it up)
"Another is that he probably doesn't spend much time working on problems that are incompletely and ambiguously described (and that can't be fixed in a meaningful time and/or budget), part of an ad–hoc domain, intrinsically fuzzy, aiming or a moving target from a moving platform, subject to capricious and arbitrary constraints, etc. etc. etc."
You mean like TeX and Metafont?
I would never write a program like Knuth wrote TeX, but I learned a hell of a lot from reading the source code.
Completely agree that Knuth's comments make sense for the way he works and not for the way most modern software engineering works.
I have seen and heavily used much production code from "famous" people that claimed to invent or at least advance test driven development. No, these people don't write much code anymore, but when they did, guess what? Yep, no test code; none. But their code worked well. What has changed? Time. Rate of Development. Number of people and things we integrate with. These changes all mandate test code. Sorry smart folks...but this is the way of our current world.
"You mean like TeX and Metafont?"
OK, we'll amend this. There are 2 types of programs Knuth writes. Those which are fairly well-defined, and those which run over schedule by a decade.
I'll be the first to proclaim that TeX is a great program, but I don't know many employers who would approve that approach to software, if you proposed it to them.
Knuth writes ambiguously-defined programs by taking a year to define it and then 10 years to implement it. That's a great way to write bug-free code, but I suspect your employer still doesn't want you to pull a Knuth. :-)
"CurmudgeonlyTroll said...
Beware of bugs in the above code; I have only proved it correct, not tried it. - Donald Knuth (look it up)"
Dijkstra said that, DO look it up (The Humble Programmer, Edsger Wybe Dijkstra).
-- dsl
"coödinating"
Looks like you replaced the "r" with some kind of umlaut.
missing 'r' fixed. Thanks.
Nice commentary on the unit testing comments. I couldn't have said it better.
++Alan
jhi's comment reminds me of the witticism, "In theory, there is no difference between theory and practice. In practice, there is."
"Knuth writes ambiguously-defined programs by taking a year to define it and then 10 years to implement it."
Knuth decided to write TeX in Feb 1977, started the design in May 1977, had it mostly coded by Oct 1977, finished the first draft of the code on Feb 1978 (with time out for creating fonts), and debugged it during Mar 1978 [see his essay "The Errors of TeX"]. Obviously there was plenty of work done after that too, but TeX was written pretty damn fast.
Knuth: Nothing needs to be "mocked up."
This from a man who wrote the algorithms in TAOP in the assembly code of an entirely fictitious processor!
To follow up what James Iry wrote, I don't think static type systems are the low hanging fruit.
Decades of research into static type systems haven't made them any easier to use. Haskell's type inference is a good example. If you don't write explicit type constraints you can end up with a type inference error somewhere in your code. Where? The only way to find out is to incrementally add explicit type constraints (using binary chop, for example) to narrow down where the error is. It's not much different, and no easier, than using printf for debugging C code. The easiest way to avoid this problem is to add explicit type constraints as you work, which ends up being no better than Java (and worse in some ways because Haskell makes you duplicate identifiers to define their types).
And after all that, they don't help you solve the problems that formal methods are really helpful for: detecting errors at design time that cannot be easily tested for. E.g. concurrency problems.
The best tool I've found so far that brings formal methods to the working programmer is FindBugs, which really does find bugs very well by static analysis.
Post a Comment