8 ms·

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

74 points by gnosis 16y ago

ShardPhoenix 16y ago
But is he yet, or still, right? Do formal methods really matter? Are they even possible for realistic problems?
- diN0bot 16y 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-vaillant 16y 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 16y 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/terminator/ http://research.microsoft.com/en-us/um/cambridge/projects/te...
- gills 16y 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.
luu 16y 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.
- tome 16y 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?
  - luu 16y 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.
    - dragoon 16y ago
      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.
lifeisstillgood 16y 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.
deleted 16y ago
[deleted]
limist 16y 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 16y 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-vaillant 16y 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.)
  - kiujygtyujik 16y 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
    - sqrt17 16y ago
      A bridge that depends on all rivets being perfect is a bad thing. A proof that no longer holds outside of its domain of application is still useful. The trick is to recognize when you need one and when you'd rather use the other.
limist 16y 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 16y ago
  You might want to look at something like: http://en.wikipedia.org/wiki/Formal_semantics_of_programming_languages 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 16y 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/ http://mitpress.mit.edu/algorithms/ [2] http://www.cs.au.dk/dADS1/daimi-fn64.pdf http://www.cs.au.dk/dADS1/daimi-fn64.pdf
  - drothlis 16y 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 http://www.elementsofprogramming.com/book.html
    - limist 16y ago
patio11 16y 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 16y 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 16y ago
He's right. One should never anthropomorphise computers, they hate that!
stuhacking 16y 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.
awakeasleep 16y 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).

74 points by gnosis 16y ago

ShardPhoenix 16y ago

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

diN0bot 16y 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-vaillant 16y 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 16y 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/terminator/ http://research.microsoft.com/en-us/um/cambridge/projects/te...
gills 16y 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.

luu 16y 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.

tome 16y 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?
- luu 16y 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.
  - dragoon 16y ago
    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.

lifeisstillgood 16y 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.

deleted 16y ago

[deleted]

limist 16y 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 16y 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-vaillant 16y 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.)
- kiujygtyujik 16y 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
  - sqrt17 16y ago
    A bridge that depends on all rivets being perfect is a bad thing. A proof that no longer holds outside of its domain of application is still useful. The trick is to recognize when you need one and when you'd rather use the other.

limist 16y 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 16y ago
You might want to look at something like: http://en.wikipedia.org/wiki/Formal_semantics_of_programming_languages 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 16y 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/ http://mitpress.mit.edu/algorithms/ [2] http://www.cs.au.dk/dADS1/daimi-fn64.pdf http://www.cs.au.dk/dADS1/daimi-fn64.pdf
- drothlis 16y 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 http://www.elementsofprogramming.com/book.html
  - limist 16y ago

patio11 16y 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 16y 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 16y ago

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

stuhacking 16y 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.

awakeasleep 16y 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).