3 ms·

> [...] using appropriate pre/post conditions. A good example can be seen in the use of Design-by-Contract syntax in Eiffel. I agree that these have some promi

> [...] using appropriate pre/post conditions. A good example can be seen in the use of Design-by-Contract syntax in Eiffel. I agree that these have some promise, but there is a rather wide gap between those and correctness proofs, and I'm not convinced that's a gap generally worth bridging. > One has to remember that when Dijkstra did these almost nothing that we take for granted today existed And yet at that time, he was capable of writing an ALGOL 60 compiler in assembly language within a few months. Two decades later, armed with his complete arsenal of program correctness techniques, he spent weeks writing an toy expression parser in a high level language, abandoned his original objective along the way, and ended up with an absolute dog's breakfast of impenetrable prose and code: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/EWD550.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E... Compare, for instance, how Wirth presents an overlapping subject in a straightforward manner: https://people.inf.ethz.ch/wirth/CompilerConstruction/CompilerConstruction1.pdf https://people.inf.ethz.ch/wirth/CompilerConstruction/Compil... Which of these two coding styles would you rather see in a PR?

rramadass 4y ago
You have now shifted goalposts and are arguing about things different from the ones you started with. There doesn't seem to be anymore to discuss about and so i will end this with the following notes. Your original contention that Dijkstra had not written much code (thus insinuating that he was mostly "talk") i have proven false. Incidentally, he wrote about 1318 EWDs totaling over 7700 pages in addition to his other books and papers (most of them have some "program pseudo-code")! This is indeed some impressive output. I had also pointed out that much of his work is at a "meta-level" trying to get at the nature of programming and trying to establish that discipline on a sound mathematical basis. Thus it cannot be compared directly to conventional programing but one has to understand the intent behind his writings and then try to practice them honestly in one's own work. He did not claim that his methods were "easy" only that they were a necessity to write "correct" programs. The degree to which they are necessary and applicable by "ordinary programmers" (i.e. w/o too much mathematical maturity) can be tuned (hence my example of DbC from Eiffel). From Mathematics we all know the difficulty of writing and reading proofs. So your expectation that Dijkstra's usage of it should be easy to grasp is fundamentally wrong. It is the nature of the subject itself that demands effort and there is no getting around it. Incidentally while i am somewhat familiar with Wirth's compiler book (written for students), i have not read EWD550(seems to be written as a challenge response and quite intricate/non-trivial). It seems that they have very different purposes and audiences in mind and so a comparison between them is not fair.
- microtherion 4y ago
  > Your original contention that Dijkstra had not written much code (thus insinuating that he was mostly "talk") I could have been clearer about this, yes. I know that he was quite skilled at writing code in his younger years. However, he largely seemed to have given up on the practice by the 1970s, and the less he was coding, the more certain he seemed to become how it ought to be done and taught. > From Mathematics we all know the difficulty of writing and reading proofs. So your expectation that Dijkstra's usage of it should be easy to grasp is fundamentally wrong. So the supposedly superior methodology is neither easier to use, nor does it produce easier to maintain programs. It's almost like its superiority consists purely of gatekeeping the programming profession to those conversant with the methodology's shibboleths. > I have not read EWD550 I should have led with that. As far as I know, it's the longest published program to which Dijkstra tried to apply his methodology, so, to me, the clearest evidence that it does not scale.
  - rramadass 4y ago
    You now seem to be trying to argue the inarguable and also trying to play "gotcha" games. To take the latter first, because EWD550 is intricate and unfinished, is it your contention that Dijkstra was wrong about his methodology which he had already demonstrated in other papers and books? This is not an argument but only calls into question one's own current competency and effort put forth to understand what has been written down. I am sure that if one sits down with it for concentrated study for some time that one can understand it. People lose interest in many things that they take up. This is even more true of geniuses since they have so much going on that once they have understood the gist of something they move on and leave the rest as "an exercise for the reader". They are not obligated to spell out everything for "the reader"; whether "The Reader" likes it or not is quite another matter. So to me it seems your inference on EWD550 is wrong. >So the supposedly superior methodology is neither easier to use, nor does it produce easier to maintain programs. It's almost like its superiority consists purely of gatekeeping the programming profession to those conversant with the methodology's shibboleths. Again your inference is wrong. The "superiority" lies in "proving correctness w.r.t. specification" and not in "ease of comprehension". There is no gatekeeping or any other malicious intent involved but merely insistence on a methodology. Mathematical Proofs are by definition intricate, tedious and require concentrated study. That is the nature of mathematical logic and there are no shortcuts (the famous example of Russel and Whitehead taking more than 300 pages to prove 1+1=2 comes to mind here). If one wants to follow Dijkstra's method to the letter, then one has to "up one's game". If one doesn't want to do that but get the same benefits (to a certain degree) then use a simpler approach like DbC based on the same principles but much more "user friendly". To paraphrase a famous quote: "There is no Royal Road to understanding Dijkstra".

rramadass 4y ago

You have now shifted goalposts and are arguing about things different from the ones you started with. There doesn't seem to be anymore to discuss about and so i will end this with the following notes. Your original contention that Dijkstra had not written much code (thus insinuating that he was mostly "talk") i have proven false. Incidentally, he wrote about 1318 EWDs totaling over 7700 pages in addition to his other books and papers (most of them have some "program pseudo-code")! This is indeed some impressive output. I had also pointed out that much of his work is at a "meta-level" trying to get at the nature of programming and trying to establish that discipline on a sound mathematical basis. Thus it cannot be compared directly to conventional programing but one has to understand the intent behind his writings and then try to practice them honestly in one's own work. He did not claim that his methods were "easy" only that they were a necessity to write "correct" programs. The degree to which they are necessary and applicable by "ordinary programmers" (i.e. w/o too much mathematical maturity) can be tuned (hence my example of DbC from Eiffel). From Mathematics we all know the difficulty of writing and reading proofs. So your expectation that Dijkstra's usage of it should be easy to grasp is fundamentally wrong. It is the nature of the subject itself that demands effort and there is no getting around it. Incidentally while i am somewhat familiar with Wirth's compiler book (written for students), i have not read EWD550(seems to be written as a challenge response and quite intricate/non-trivial). It seems that they have very different purposes and audiences in mind and so a comparison between them is not fair.

microtherion 4y ago
> Your original contention that Dijkstra had not written much code (thus insinuating that he was mostly "talk") I could have been clearer about this, yes. I know that he was quite skilled at writing code in his younger years. However, he largely seemed to have given up on the practice by the 1970s, and the less he was coding, the more certain he seemed to become how it ought to be done and taught. > From Mathematics we all know the difficulty of writing and reading proofs. So your expectation that Dijkstra's usage of it should be easy to grasp is fundamentally wrong. So the supposedly superior methodology is neither easier to use, nor does it produce easier to maintain programs. It's almost like its superiority consists purely of gatekeeping the programming profession to those conversant with the methodology's shibboleths. > I have not read EWD550 I should have led with that. As far as I know, it's the longest published program to which Dijkstra tried to apply his methodology, so, to me, the clearest evidence that it does not scale.
- rramadass 4y ago
  You now seem to be trying to argue the inarguable and also trying to play "gotcha" games. To take the latter first, because EWD550 is intricate and unfinished, is it your contention that Dijkstra was wrong about his methodology which he had already demonstrated in other papers and books? This is not an argument but only calls into question one's own current competency and effort put forth to understand what has been written down. I am sure that if one sits down with it for concentrated study for some time that one can understand it. People lose interest in many things that they take up. This is even more true of geniuses since they have so much going on that once they have understood the gist of something they move on and leave the rest as "an exercise for the reader". They are not obligated to spell out everything for "the reader"; whether "The Reader" likes it or not is quite another matter. So to me it seems your inference on EWD550 is wrong. >So the supposedly superior methodology is neither easier to use, nor does it produce easier to maintain programs. It's almost like its superiority consists purely of gatekeeping the programming profession to those conversant with the methodology's shibboleths. Again your inference is wrong. The "superiority" lies in "proving correctness w.r.t. specification" and not in "ease of comprehension". There is no gatekeeping or any other malicious intent involved but merely insistence on a methodology. Mathematical Proofs are by definition intricate, tedious and require concentrated study. That is the nature of mathematical logic and there are no shortcuts (the famous example of Russel and Whitehead taking more than 300 pages to prove 1+1=2 comes to mind here). If one wants to follow Dijkstra's method to the letter, then one has to "up one's game". If one doesn't want to do that but get the same benefits (to a certain degree) then use a simpler approach like DbC based on the same principles but much more "user friendly". To paraphrase a famous quote: "There is no Royal Road to understanding Dijkstra".