A desirable property of techniques to improve task success is that it is actually implementable by the people carrying out the tasks. Formally proving the correctness of CRUD apps leaves something to be desired here. (To say nothing about formally proving the correctness of the browser and underlying OS, which is probably a necessary pre-requisite of proving the correctness of the CRUD app.)
One of the reasons statistics took Japanese manufacturing by storm is that you can, and Toyota does, teach everything you need to know to justify pushing the Big Red Button to someone with a high school math background. ("Here's a graph for the stat of interest. For each production run, test one and put an X on this graph. If you see three Xs above this line, the process is out of control. Anyone in the factory who sees this, even the cleaning lady, should immediately walk over and push the Big Red Button, costing us hundreds of millions of yen. You will not get in trouble, indeed, we will praise you for diligence. Why does this work? Stats 101 lecture.")
I disagree with Dijkstra on the big picture, but it's amazing how many nuggets of wisdom this essay contains.
For instance, this passage gets across the main idea of Joel's leaky abstractions essay in just one short paragraph, almost two decades before Joel wrote his essay
It is possible, and even tempting, to view a program as an abstract mechanism, as a device of some sort. To do so, however, is highly dangerous: the analogy is too shallow because a program is, as a mechanism, totally different from all the familiar analogue devices we grew up with. Like all digitally encoded information, it has unavoidably the uncomfortable property that the smallest possible perturbations —i.e. changes of a single bit— can have the most drastic consequences. In the discrete world of computing, there is no meaningful metric in which "small" changes and "small" effects go hand in hand, and there never will be.
"Abstractions leak" is pretty far from what I got out of that paragraph. Actually, I don't think leaky abstractions have much to do with the fact that small changes have large consequences.
In the discrete world of computing, there is no meaningful metric in which "small" changes and "small" effects go hand in hand, and there never will be.
This is a fascinating quote. What's the justification for it though? Is it not possible that one day we will invent a computer language that supports writing very "robust" (in the sense of source code sensitivity) programs?
Isn't that, in many ways, the opposite of what people want out of a programming languages? It seems to me that expressiveness, and robustness (in the sense that you define robustness) are inversely related.
Whenever a language comparison pops up, there's always a large contingent of people who argue for the superiority of a language because ideas can be expressed more concisely in 'their' language, but that necessarily means that some small change will have a relatively large effect.
There's also robustness in the sense that, e.g., BitC was trying to be robust, and that's something that I think is promising.
However, a concise, expressive, very high-level domain-specific language can make it impossible to express many idioms that would break the semantics of the domain.
As an analogy (I hesitate to use one because of the article), you could have a high-level representation of HTML that would make it totally impossible to generate <HTML></NOTHTML>, which is not the case if you use a general-purpose system. (not a foolproof analogy but anyway)
On formal principles, we'd expect that robustness and expressiveness are inversely related, on the principle that low-entropy data can be recovered with better fidelity than dense data, but I think I can name a counterexample to this principle in practice: I think Haskell does a phenomenally good job of being both expressive and robust if we consider a practical definition of robust, whereby pain is not measured by likelihood of error but the cost of an error. Compile-time errors are extremely cheap in comparison to run-time errors.
You want an "almost right" program to fail, but you want it to do so at compile time. Runtime silent failure is the worst.
How could it be possible? Let's assume that a "small effect" is something like a character change. Consider:
if (a == b) ...
And,
if (a != b) ...
One character difference, exactly opposite meaning. Is it possible for such behavior to not exist in programming languages? I can't prove it, but I doubt it. I suspect it's inherent.
Let me clarify. Consider if I instead chose equal and not equal as my operators. Now a "small change" probably won't even be a valid program (not wqual). Any small change that does result in a valid program is unlikely to result in an equally small behavior change for any interesting input. Changing a strictly-less-than to a less-than-or-equal-to is a small change that results in what seems like a small behavior change when viewed locally. But my own experience with programming is that a local change such as that will have huge consequences later on - often to the point that the program crashes.
Consider it this way: the space of valid programs is infinite. The space of valid programs that solve a particular problem is much smaller (in the physics << sense) than the space of valid programs. Any perturbation from a valid program that solves the problem is much more likely (>>) to land you on a valid program that does not solve your problem than one that does.
I agree with your intuition, but computer science is a mathematically founded discipline, so the kinds of claim Dijkstra was making about "robustness" require formalisation and mathematical proof if they are to be taken seriously.
Like you I find it very difficult to even envisage what a "robust" language would be in this sense. What I'd like is for someone to define the properties that one would have and then show that it can't exist :)
NB he is demonstrably incorrect on this point:
Like all digitally encoded information, it has unavoidably the uncomfortable property that the smallest possible perturbations —i.e. changes of a single bit— can have the most drastic consequences.
>>> Like all digitally encoded information, it has unavoidably the uncomfortable property that the smallest possible perturbations —i.e. changes of a single bit— can have the most drastic consequences.
>> Error correcting codes do exist!
He acknowledged this explicitly immediately after, on the next sentence:
> [For the sake of completness I add that the picture is not essentially changed by the introduction of redundancy or error correction.]
Think of what happens if a single bit is changed in the error-correcting part of the program.
You could once-and-for-all prove the error correcting program correct and then use it again and again for every program. But that wouldn't actually help getting programs correct. For example if your error correcting program was to write every program three times, then if one of the three programs gives a different answer you use the answer of the other two. Now a human writing a program would probably just write the same bug in each of the three versions, i.e. the three versions are not independent. You could have the three versions written by three different humans. But that doesn't solve the problem either because some errors are just likely to be made by all three of them (for example forgetting to check some edge condition somewhere). So again the three versions are correlated. Or worse the problem could be in the specification all three of them got. I don't think there is any way out of this.
Human DNA is a "robust language." Everything is encoded redundantly, and most features "express" through multiple small, additive gates (e.g. changing one bit of your DNA will never take your hair all the way from blonde to black, only make it slightly lighter or darker.) We could make a programming language that works similarly, though it would likely be very unintuitive.
Not everything is encoded redundantly. Try changing CGA to TGA in one of the exons of PAX6. In humans, this change will result in aniridia, the lack of an iris, an unstable corneal epithelium, and other problems. This is just one example, the one I'm familiar with. There are many other single nucleotide polymorphisms that can cause big changes.
We think in continuous terms all the time when we use big O notation. If you have an O(n) (or O(n^2)) algorithm and make the input a tiny bit bigger, the computation becomes a tiny bit more complex. Dijkstra is too rigorous to let us get away with that, though. In theory, big O notation says nothing about any particular finite value, only about limits, and in practice, this manifests in big O notation's failure to predict big jumps in resource costs when internal limits such as cache sizes are exceeded. To create an abstraction as nice and well-behaved as big O notation, we have to gloss over the real behavior of the machine.
Is it not possible that one day we will invent a computer language that supports writing very "robust" (in the sense of source code sensitivity) programs?
If you apply an edit distance metric to source code and a behavior metric to running programs, it would take a ridiculous amount of work to write programs in any system where small changes in source code resulted in small changes in running systems. Also, very often people want small changes in input data to result in small changes in behavior, but just as often, they want small changes in input data to result in large changes in behavior, so we have external requirements to make some parts of our program "robust" and other parts extremely sensitive. A language would need to support both requirements.
I do believe we could simulate that, for some users, but we could never do it in any meaningful way in the context of this discussion.
For instance, we could make a language that interpreted "plus", "+", "adds", and "pslu" as addition operators. But that would only be increasing the amount of operators.
Even if we had an adaptive algorithm that would figure out what people meant in context, it would only reduce the amount of syntax errors.
What is really referred to here is the elements of the program. In this example, it would be our decision to add. If that elemental decision was wrong, the program would flip.
Another case is to consider numbers. If a letter needs to be mailed to every fifth address, and the elemental data, 5, is altered in any way, the program will fail. So while our algorithm could pick up 'fiev' and 'fifth', 4 or fourth will blow it.
I think luu is underestimating Mr Dijkstra - this one essay has more nuggets than Mcdonalds...
I prefer to describe it the other way round: the program is an abstract symbol manipulator, which can be turned into a concrete one by supplying a computer to it.
if we wish to count lines of code, we should not regard them as "lines produced" but as "lines spent"
As economics is known as "The Miserable Science", software engineering should be known as "The Doomed Discipline"
and so on.
You can happily read most of the current problems we face in the Doomed Discipline laid out 30 years ago.
In the end, reading honest thinking from people orders more intelligent than yourself always inspires something.
Worth reading just to receive the wisdom of this change of perspective - I'm going to stop calling my errors "bugs":
We could, for instance, begin with cleaning up our language by no longer calling a bug a bug but by calling it an error. It is much more honest because it squarely puts the blame where it belongs, viz. with the programmer who made the error. The animistic metaphor of the bug that maliciously sneaked in while the programmer was not looking is intellectually dishonest as it disguises that the error is the programmer's own creation. The nice thing of this simple change of vocabulary is that it has such a profound effect: while, before, a program with only one bug used to be "almost correct", afterwards a program with an error is just "wrong" (because in error).
> while, before, a program with only one bug used to be "almost correct", afterwards a program with an error is just "wrong" (because in error).
So almost every program is "wrong" then. This is pretty pessimistic. Every glass is empty unless it is 100% full.
I think the better approach is just to not fool ourselves. If a large application works, but has a few bugs, then it's OK to say that it's 90% working (or 10% broken--have your pick).
If you can say that an application is 90% working, then you can probably divide it into at least two cleanly separated parts: one that works, and one that is erroneous. So, the more correct way to state this would be that x% of your program works. (Unfortunately for you, x may be much lower than 90. Think edge cases.)
This is related to Dijkstra's suggested style of programming. He suggested, or in fact insisted that the proper way to program is to create along with each program mathematical proofs that the program will behave as expected under each possible combination of inputs. This is something that might conceivably result in bug free programs.
Needless to say this style was not adopted, and in fact a very very different style that practically guarantees a lot of bugs was used.
So the expectation that programs be perfect seems impossible now, but it was not for Dijkstra considering the style of coding he had in mind.
You are kidding me right? If we change this, then each time there is a bug in your program your manager gets to blame you, your clients won't pay you until fix what you have done wrong, you might be open to lawsuits, etc, etc.
Yeah it might be a lot more honest - but it would be very impractical.
Firstly, errors can stem from the "client side." Few software specifications are so precise that solutions can be proven complete and correct. So I don't think an honest programmer has to lie about errors; but one would need to regularly educate the "client" that most development is an iterative process of discovery, with everyone learning and saying "Oh but what I really want it to do is x..."
Secondly, I've never met a good/great programmer who wasn't honest with himself first. Coding always involves fixing errors (heh, I was about to say "debugging") and by some studies (e.g. as cited in Code Complete), > 99% of code errors are programmer errors (not the OS, not the compiler/interpreter, etc.). I think the transition of internal dialog from "WTF, why is SELECT broken?" to "Hummm, what assumption of mine is wrong?" is vital. Changing one's terminology, even if it's just in the space between your own ears, will help us as programmers improve sooner.
...the subculture of the compulsive programmer, whose ethics prescribe that one silly idea and a month of frantic coding should suffice to make him a life-long millionaire
for real formal methods it's a trade off that only those who really need security or reliability might practically make, eg banks and space agencies.
however, i think there is a continuum of methods, from TDD to proving correctness. it is often practical in the real world to do up front design before hacking out some code. i believe super smart hackers actually make lots of smart design decisions when "hacking" out code, whether that is realizing the appropriate loop invariants to make an algorithm work or figuring out the right abstractions for reusable code. there's lots of ways that good forsight produces correct code faster. that's what intelligence is: thinking, not brute force.
the smart coder, especially after gaining a variety of experiences and learning from different mentors, takes pieces of different methods in order to simultaneously make headway on different goals, not just correctness and extensibility, but refactorability, fast-rampup for new team members, fun, etc.
The trade off you speak of rely on the unspoken assumptions that (0) applying formal methods costs more than not to, and (1) the astonishing complexity of our programs is actually needed.
I highly doubt (0), at least when you take into account the costs of errors: crashes, wrong results, security breaches… These costs impact the user instead of the programmer, but they are costs nonetheless (plus, letting customers pay for these strikes me as not nice).
I highly doubt (1), at least when you take into account our overusing of low level programming languages, and of course anthropomorphic thinking.
In my opinion, one of the big problems with formal methods is getting the specification right. You might be able to prove that your program conforms to your specification, but what is to say that your specification is any less buggy than your program? Some interesting work has been done with proving that certain errors do not occur, rather than proving the entire program correct. For instance, Microsoft's Terminator project [1] is used to prove that device drivers do not hang.
I think that formal methods do matter, and can be realistic. We have a culture problem, perhaps inherent to the ease with which programs of unknown correctness may be written and executed, that usually we just don't care. How familiar is this cycle? iterate{think => type => execute => check}? Being rushed into the "protoduction" dev model doesn't help a lot either.
I had a professor who was apparently a student of E.W. Djikstra, and many of the points in this essay were essential to his courses. For example, exam questions weren't just "write code to do X", but "write code to do X and prove it", with failure to prove it resulting in a big fat 0. Of course, we were required to use weakest-precondition verification, from the bottom to the top. Not as tedious as it sounds, once you've gone through it once or twice, and I think the point wasn't to teach something we would use day-to-day, but to teach us that verifying programs by hand was not only possible but tractable. It seems like the TDD movement kind of makes the same point, though perhaps less formally.
Another professor introduced a variant of this technique developed for verifying the critical points of parallel and multi-threaded computation, which while far more tedious has been vastly more useful in my career as a model for thinking about concurrent programs [not bulletproof, of course, because runtimes and hardware sometimes do unexpected but perfectly valid things with our programs].
Most algorithms, at their core, have formal descriptions short enough to prove by hand in a matter of minutes. For those parts, I think it's realistic to use formal methods. All the other cruft we tack on to our programs to make then flexible, perform in a variety of contexts, handle varying data types, error checking, etc.; I think those fall in the realm of what you describe as "realistic programs", and which amounts to a daunting heap of code to verify by hand. Luckily, we can again follow his advice and use computation as an alternative, and verify by hand a program which can verify some or most of our work for us -- that seems to be what a lot of static analysis is all about.
I don't know. Do you ever run into situations day to day where you find yourself verifying your code by hand? That's usually what happens when I get deep into finding an error.
>It is misleading in the sense that it suggests that we can adequately cope with the unfamiliar discrete in terms of the familiar continuous, i.e. ourselves, quod non. It is paralyzing in the sense that, because persons exist and act in time, its adoption effectively prevents a departure from operational semantics and thus forces people to think about programs in terms of computational behaviours, based on an underlying computational model. This is bad, because operational reasoning is a tremendous waste of mental effort.
I don't get the part where thinking in terms of computational behaviors throws something off (and more).
Where and how can one effectively learn the kind of formal reasoning he describes, and that he mentions having taught to college freshmen? Could a knowledgeable HN'er please give follow-up resources? Thanks!
I was introduced to formal reasoning about programs in an introductory course on algorithms and data structures in March. Most of the curriculum was from CLRS,[1] which presents proofs of correctness for many algorithms but doesn't explain how to develop such proofs. The curriculum for the last two weeks of the course, however, was a handout titled Transition Systems,[2] which I found to be an excellent introduction to the subject.
Since that time I've been interested in the idea of proving programs correct. On weekends I'm currently making my way through David Gries's The Science of Programming. Similar books include
I think category theory could be the maths for software engineers to the mechanical engineers calculus. Once you get past the arrows and weird Greek nomenclature you realize its just algebra. It seems a reasonable compromise to using formal logic whose cost is simply not worth it in most all cases. Still most presentations are very academic and neither presented in the way that a busy engineer can easily grasp and use. I've been trying to simultaneously learn and break it down to a much simpler core for my self that can be used without thinking - kind of like how engineers use physics - but still serve as a strong scaffolding of support when attacking a problem. Progress is tough though.
I seem to remember that Dijkstra was keen on identifying weakest preconditions of different statements that can be used to prove a program correct.
However, I warn you that if you try this you will soon find out what this kind of formal reasoning about programs never caught on that widely - at least for imperative programs.
On one hand, they're wonderfully blunt and unforgiving. I see in their contents statements that I agree with, but also very strict ideas that I know I've broken in the past. I suppose then that reading the EWDs is usually a guilty pleasure.
One the other hand, it would be very difficult to actually employ a lot of his best practice ideas due to the complexities of working in team environments with differently minded colleagues against tight deadlines. Trade-offs have to be made, unfortunately.
One of the reasons statistics took Japanese manufacturing by storm is that you can, and Toyota does, teach everything you need to know to justify pushing the Big Red Button to someone with a high school math background. ("Here's a graph for the stat of interest. For each production run, test one and put an X on this graph. If you see three Xs above this line, the process is out of control. Anyone in the factory who sees this, even the cleaning lady, should immediately walk over and push the Big Red Button, costing us hundreds of millions of yen. You will not get in trouble, indeed, we will praise you for diligence. Why does this work? Stats 101 lecture.")