3 ms·

This speech was so quintessentially Dijkstra. Here's where it got super-Dijkstra: > Right from the beginning, and all through the course, we stress that the pr

This speech was so quintessentially Dijkstra. Here's where it got super-Dijkstra: > Right from the beginning, and all through the course, we stress that the programmer's task is not just to write down a program, but that his main task is to give a formal proof that the program he proposes meets the equally formal functional specification. And so we produce programmers who are helpless without formal functional specifications, and are therefore incapable of writing any software in the real world, with conflicting, underspecified, and post-hoc requirements. But more importantly: this sucks all of the joy out of it! Who here got into programming out of a passion for translating formal functional specifications into formal proofs? How can any of the magic of software survive such a mindset?

a1369209993 11y ago
If you don't have a formal functional specification that adequately characterizes the program's behavior, then Dijkstra's approach is useless. If you do have a formal functional specification that adequately characterizes the program's behavior, then you have already have source code, and Dijkstra's approach is irrelevant.
- AnimalMuppet 11y ago
  Or at least something formally equivalent to source code, even if there is not a "compiler" for it. But then the programmer becomes merely a human compiler, doing a provably-formally-equivalent transform to a formal specification. Even if Dijkstra's approach is not irrelevant, it is inhuman - it makes the programmer into a machine. (Note that the first "computers" were human machines.)
agumonkey 11y ago
Honest question, isn't it a historical bias ? maybe in his days programming projects were devoted to huge, complex and costly problems that were always pretty strictly defined, unlike the late 70s ~Apple/Microcomputer days ? > But more importantly: this sucks all of the joy out of it! Who here got into programming out of a passion for translating formal functional specifications into formal proofs? How can any of the magic of software survive such a mindset? Sure, but I do like the bliss of watching a tiny piece of code knowing it's sound by induction.
- AnimalMuppet 11y ago
  > maybe in his days programming projects were devoted to huge, complex and costly problems that were always pretty strictly defined, unlike the late 70s ~Apple/Microcomputer days ? Huge? Not by today's standards. Complex? Again, not by today's standards, but they didn't have today's libraries to build on. Costly? Definitely. Pretty strictly defined? They tried to be, but the gaps always showed. Certainly they were not strictly defined by Dijkstra's standards.
JadeNB 11y ago
> And so we produce programmers who are helpless without formal functional specifications, and are therefore incapable of writing any software in the real world, with conflicting, underspecified, and post-hoc requirements. That … doesn't seem like a problem that exists in the world as it exists (but see the caveat below on my qualification to make such statements). It seems like the real world of programming is so full of people who are so used to conflicting, underspecified, and post hoc requirements that it doesn't occur to them that there is any other way, and so we live in a world in which it is simply assumed that software doesn't actually work as it is supposed to do, even if only in edge cases. Should all software be formally specified? No, and I'm sure that, despite his passion for overstatement, even Dijkstra didn't think so—but I think that the programming world would probably be a better place if more programmers were aware of the potential and possibility of formalisation, and so could introduce and take advantage of it as appropriate. > But more importantly: this sucks all of the joy out of it! Who here got into programming out of a passion for translating formal functional specifications into formal proofs? Me! I think it's not fair to assume that everyone enjoys programming for the same reason that you do, any more than it would be for Dijkstra to assume that others do or should for the same reason that he did. To be fair, though, I'm a mathematician, not a professional programmer.
jonjacky 11y ago
If you can get past Dijkstra's arrogance and abrasive presentation, he actually has some useful things to teach. If you look at one of the books where he and his colleagues teach how to do this (for example, A Method of Programming, by Dijkstra and Fiejen) it's pretty clear that the programmer him(her)self is supposed to come up with the formal specification. Much of the book is about how to write the specifications. The formal specifications are just assertions - they are Boolean expressions that express properties of the solution. For example the formal specification for a square root function might be abs(r*r - x) < d, where x is the number, r is the root, and d is an error tolerance. In general these formal specifications cannot be mechanically compiled into an executable program - they are nonconstructive - like the square root example above. So you still have to find or invent an algorithm. An interesting feature of Dijkstra's method is, he does suggest some heuristics for getting from the assertions to the code, that can help you discover an algorithm. They remove the mystery surrounding how some non-obvious algorithms were discovered. Dijkstra's approach is actually a lot like test-driven development - the idea is, you start with some assertions that describe what the code is supposed to do, then you check the assertions as you go -- instead of writing a bunch of code and checking it at the end. The difference is just how you check the assertions - by running tests or by attempting a proof. Test cases are formal specifications too - they are just incomplete - somebody said they are 'specification by example'.

a1369209993 11y ago

If you don't have a formal functional specification that adequately characterizes the program's behavior, then Dijkstra's approach is useless. If you do have a formal functional specification that adequately characterizes the program's behavior, then you have already have source code, and Dijkstra's approach is irrelevant.

AnimalMuppet 11y ago
Or at least something formally equivalent to source code, even if there is not a "compiler" for it. But then the programmer becomes merely a human compiler, doing a provably-formally-equivalent transform to a formal specification. Even if Dijkstra's approach is not irrelevant, it is inhuman - it makes the programmer into a machine. (Note that the first "computers" were human machines.)

agumonkey 11y ago

Honest question, isn't it a historical bias ? maybe in his days programming projects were devoted to huge, complex and costly problems that were always pretty strictly defined, unlike the late 70s ~Apple/Microcomputer days ? > But more importantly: this sucks all of the joy out of it! Who here got into programming out of a passion for translating formal functional specifications into formal proofs? How can any of the magic of software survive such a mindset? Sure, but I do like the bliss of watching a tiny piece of code knowing it's sound by induction.

AnimalMuppet 11y ago
> maybe in his days programming projects were devoted to huge, complex and costly problems that were always pretty strictly defined, unlike the late 70s ~Apple/Microcomputer days ? Huge? Not by today's standards. Complex? Again, not by today's standards, but they didn't have today's libraries to build on. Costly? Definitely. Pretty strictly defined? They tried to be, but the gaps always showed. Certainly they were not strictly defined by Dijkstra's standards.

JadeNB 11y ago

> And so we produce programmers who are helpless without formal functional specifications, and are therefore incapable of writing any software in the real world, with conflicting, underspecified, and post-hoc requirements. That … doesn't seem like a problem that exists in the world as it exists (but see the caveat below on my qualification to make such statements). It seems like the real world of programming is so full of people who are so used to conflicting, underspecified, and post hoc requirements that it doesn't occur to them that there is any other way, and so we live in a world in which it is simply assumed that software doesn't actually work as it is supposed to do, even if only in edge cases. Should all software be formally specified? No, and I'm sure that, despite his passion for overstatement, even Dijkstra didn't think so—but I think that the programming world would probably be a better place if more programmers were aware of the potential and possibility of formalisation, and so could introduce and take advantage of it as appropriate. > But more importantly: this sucks all of the joy out of it! Who here got into programming out of a passion for translating formal functional specifications into formal proofs? Me! I think it's not fair to assume that everyone enjoys programming for the same reason that you do, any more than it would be for Dijkstra to assume that others do or should for the same reason that he did. To be fair, though, I'm a mathematician, not a professional programmer.

jonjacky 11y ago

If you can get past Dijkstra's arrogance and abrasive presentation, he actually has some useful things to teach. If you look at one of the books where he and his colleagues teach how to do this (for example, A Method of Programming, by Dijkstra and Fiejen) it's pretty clear that the programmer him(her)self is supposed to come up with the formal specification. Much of the book is about how to write the specifications. The formal specifications are just assertions - they are Boolean expressions that express properties of the solution. For example the formal specification for a square root function might be abs(r*r - x) < d, where x is the number, r is the root, and d is an error tolerance. In general these formal specifications cannot be mechanically compiled into an executable program - they are nonconstructive - like the square root example above. So you still have to find or invent an algorithm. An interesting feature of Dijkstra's method is, he does suggest some heuristics for getting from the assertions to the code, that can help you discover an algorithm. They remove the mystery surrounding how some non-obvious algorithms were discovered. Dijkstra's approach is actually a lot like test-driven development - the idea is, you start with some assertions that describe what the code is supposed to do, then you check the assertions as you go -- instead of writing a bunch of code and checking it at the end. The difference is just how you check the assertions - by running tests or by attempting a proof. Test cases are formal specifications too - they are just incomplete - somebody said they are 'specification by example'.