3 ms·

I try to read this paper from the perspective of his overall work and writing, and I have read through a lot of the EWDs. There is an abundance of examples that

by stiff 13y ago

I try to read this paper from the perspective of his overall work and writing, and I have read through a lot of the EWDs. There is an abundance of examples that his #1 concern was about making programming more mathematical. Hence I interpret everything that you are quoting as proposals motivated by the need he perceives of proving programs correct. That the industry trivialized his ideas to "don't use goto" does not mean this was Dijkstra's great point. This is in fact excellently summarized in the first link I posted. Meanwhile you make it sound like he was interested in contributing to software engineering like it is done today, which is not the case, he seemed to really despise a lot of the things which are now software engineering best practices, like unit tests. What I actually hoped for is someone who really learned the way of writing programs Dijkstra advocated to some extent and their experience with it. I can't say I really understand how those derivations look like in practice.

btilly 13y ago
I try to read this paper from the perspective of his overall work and writing, and I have read through a lot of the EWDs. In other words you're missing the plain meaning of the sections that I quoted because you try to consider it in the light of http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EW... which was written a decade and a half later? Pardon me, but I won't be emulating your example. The focus of Dijkstra's research career was how to make correct software. As he himself would claim, there are two halves to this process. The first is to limit ourselves to forms of writing code which are easy to reason about. The second is to actually perform that reasoning. The part of his proposal that actually had an impact is the part which says that we need to focus on methods of expressing ourselves that are easy to reason about. The part that did not have a direct impact is the part which says that we need to perform that formal reasoning. The fundamental reason why not is that Dijkstra's reasoning assumed the existence of a consistent, unchanging specification. The real world does not work that way - computers exist to do what humans ask. And humans do not always ask for things that make sense. This is not to say that this is the impact that he wanted to have - it is clearly not - but it is the impact that he did have. However some of his other ideas have indeed found their way into practice, albeit in a muted way that he would have objected to. For example take unit tests, since you brought them up. He was against tests as part of including QA as an integral part of the programming process - if the programmer performed properly then that should not be needed. (Nice theory, fails in practice.) However today, well-designed unit tests do serve as a limited form of specifying exactly what a given piece of code is supposed to do, and verifying that it in fact does that. (I'm sure that he would say limited and inadequate. But it is better than nothing.)
- stiff 13y ago
  In other words you're missing the plain meaning of the sections that I quoted because you try to consider it in the light of http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EW.. http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EW.... which was written a decade and a half later? This clearly shows you haven't actually studied his writings, because he has been raising the same points for many years in almost every EWD, OP is EWD340, so here is a sample from before this period: http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD302.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EW... http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EW... http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD317.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EW... For example from EWD317: If we take the existence of the impressive body of Mathematics as the experimental evidence for the opinion that for the human mind the mathematical method is indeed the most effective way to come to grips with complexity, we have no choice any longer: we should reshape our field of programming in such a way that the mathematician's methods become equally applicable to our programming problems, for there are no other means. It is my personal hope and expectation that in the years to come programming will become more and more an activity of mathematical nature. For a programming language to be simple in the sense of being able to prove things is a completely different thing than for it to be simple in the sense of being easy to understand informally. Yes, bastardized versions of his ideas did make it into the mainstream, I doubt it's always even because of his direct influence and that's what the wiki article I posted three comments earlier is about.

by stiff 13y ago

btilly 13y ago

I try to read this paper from the perspective of his overall work and writing, and I have read through a lot of the EWDs. In other words you're missing the plain meaning of the sections that I quoted because you try to consider it in the light of http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1036.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EW... which was written a decade and a half later? Pardon me, but I won't be emulating your example. The focus of Dijkstra's research career was how to make correct software. As he himself would claim, there are two halves to this process. The first is to limit ourselves to forms of writing code which are easy to reason about. The second is to actually perform that reasoning. The part of his proposal that actually had an impact is the part which says that we need to focus on methods of expressing ourselves that are easy to reason about. The part that did not have a direct impact is the part which says that we need to perform that formal reasoning. The fundamental reason why not is that Dijkstra's reasoning assumed the existence of a consistent, unchanging specification. The real world does not work that way - computers exist to do what humans ask. And humans do not always ask for things that make sense. This is not to say that this is the impact that he wanted to have - it is clearly not - but it is the impact that he did have. However some of his other ideas have indeed found their way into practice, albeit in a muted way that he would have objected to. For example take unit tests, since you brought them up. He was against tests as part of including QA as an integral part of the programming process - if the programmer performed properly then that should not be needed. (Nice theory, fails in practice.) However today, well-designed unit tests do serve as a limited form of specifying exactly what a given piece of code is supposed to do, and verifying that it in fact does that. (I'm sure that he would say limited and inadequate. But it is better than nothing.)

stiff 13y ago
In other words you're missing the plain meaning of the sections that I quoted because you try to consider it in the light of http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EW.. http://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EW.... which was written a decade and a half later? This clearly shows you haven't actually studied his writings, because he has been raising the same points for many years in almost every EWD, OP is EWD340, so here is a sample from before this period: http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD302.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EW... http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EW... http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD317.html http://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EW... For example from EWD317: If we take the existence of the impressive body of Mathematics as the experimental evidence for the opinion that for the human mind the mathematical method is indeed the most effective way to come to grips with complexity, we have no choice any longer: we should reshape our field of programming in such a way that the mathematician's methods become equally applicable to our programming problems, for there are no other means. It is my personal hope and expectation that in the years to come programming will become more and more an activity of mathematical nature. For a programming language to be simple in the sense of being able to prove things is a completely different thing than for it to be simple in the sense of being easy to understand informally. Yes, bastardized versions of his ideas did make it into the mainstream, I doubt it's always even because of his direct influence and that's what the wiki article I posted three comments earlier is about.