Dijkstra on the cruelty of really teaching computing science (1988)

http://userweb.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html

by gnosis • 16 years ago

74 47 16 years ago

userweb.cs.utexas.edu

But is he yet, or still, right? Do formal methods really matter? Are they even possible for realistic problems?

diN0bot• 16 years ago

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.

loup-vaillant3• 16 years ago

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.

mwilliamson• 16 years ago

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.

[1] http://research.microsoft.com/en-us/um/cambridge/projects/te...

gills• 16 years ago

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.

luu2• 16 years ago

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.

tome3• 16 years ago

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?

luu2• 16 years ago

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.

scott_s3• 16 years ago

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.

dkarl• 16 years ago

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.

awakeasleep3• 16 years ago

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.

tedunangst• 16 years ago

"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.

loup-vaillant3• 16 years ago

An abstraction that leaks is only a small change compared to the corresponding perfect abstraction. But such a small change can have big consequences.

Leaky abstractions can easily be seen a subset of what Dikstra is talking about.

lifeisstillgood• 16 years ago

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.

limist4• 16 years ago

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).

yafujifide• 16 years ago

> 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).

loup-vaillant3• 16 years ago

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.)

kiujygtyujik2• 16 years ago

Thats the difference between maths and engineering.

A proof that has a single exception is wrong, a brige that stays up with a broken rivet is correct

imran• 16 years ago

although you are right but i think you are out of context..

hristov• 16 years ago

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.

tomjen3• 16 years ago

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.

limist4• 16 years ago

"I am serious. And don't call me Shirley." :)

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.

limist4• 16 years ago

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!

arethuza• 16 years ago

You might want to look at something like:

http://en.wikipedia.org/wiki/Formal_semantics_of_programming...

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.

jhck• 16 years ago

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

- A Discipline of Programming by Dijkstra

- The Evolution of Programs by N. Dershowitz

[1] http://mitpress.mit.edu/algorithms/

[2] http://www.cs.au.dk/dADS1/daimi-fn64.pdf

drothlis• 16 years ago

In a similar vein is Elements of Programming by Alexander Stepanov (designer of the C++ STL) and Paul McJones: http://www.elementsofprogramming.com/book.html

Dn_Ab• 16 years ago

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.

patio11• 16 years ago

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.")

helmut_hed• 16 years ago

When he says this:

...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

I feel like he's describing many a startup today.

konad• 16 years ago

He's right. One should never anthropomorphise computers, they hate that!

stuhacking• 16 years ago

I enjoy Dijkstra's essays.

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.

awakeasleep3• 16 years ago

Could anyone explain what Dijkstra meant by

>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).

Dijkstra on the cruelty of really teaching computing science (1988)

Related Stories