4 ms·

> But his fundamental thesis that a "Program" should be treated as a mathematical object and proved using rigorous logic is still true How is that even remotel

by adwn 6y ago

> But his fundamental thesis that a "Program" should be treated as a mathematical object and proved using rigorous logic is still true How is that even remotely true? How are you going to formally model a browser, or a word processor, or your mail client, or a 3D game, let alone prove it correct against that specification? If we actually followed that requirement, computers would be almost useless today, except for a few tiny niches where millions of dollars in development costs for even relatively small programs would be justified. Keep in mind that your development tools would be meager to non-existent as well, since they'd also have to satisfy that overly strict requirement.

TheOtherHobbes 6y ago
Quite. It's the silliest of silly ideas - not just practically, but conceptually, because real problems don't have hard algorithmic edges. Which is why they're so hard. Don't forget there's a difference between a formal (user) specification and a functional specification. A functional specification says that when you select "Edit -> Cut" the user can expect certain things to happen. A formal specification defines how the symbolic entities involved in implementing the operation should operate. This isn't too hard for "Edit -> Cut", but it's not tractable at all for "Translate this poetry into another language without mistakes or ambiguities." So in fact he's just as guilty of resorting to metaphor as anyone else in computing. Only in this case the metaphor is the algorithmic perfection and consistency of a mathematical proof. This is fine in the classroom and in certain applications where formal methods can help, but not so much in the average developer room. It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets. But I expect he'd have dismissed that idea as too dangerously novel.
- rramadass 6y ago
  >It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets. Not quite. Computers only deal with Symbolic Logic via Formal Systems. The mapping of those to a Domain of Discourse is the job of the Programmer.
rramadass 6y ago
Here is Dijkstra himself answering the charge via EWD288 - "Concern for Correctness as a Guiding Principle for Program Composition". Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. In the step-wise approach it is suggested that even in the case of a well-defined task, certain aspects of the given problem statement are ignored at the beginning. This means that the programmer does not regard the given task as an isolated thing to be done, but is invited to view the task as a member of a whole family; he is invited to make the suitable generalizations of the given problem statement. By successively adding more detail in the lower levels he eventually pins his program down to a solution for the given problem. You can also find some relevant discussion (including my posts) at https://news.ycombinator.com/item?id=24942671 https://news.ycombinator.com/item?id=24942671 The point is that by using a top-down and step-wise refinement methodology one can show "correctness" at whatever level of granularity is acceptable.
- adwn 6y ago
  What would a coarse-granular specification for Excel look like? How would you prove correctness against such a spec? Examples, please. In these discussions, I only ever see vague statements and handwaving by formal verification proponents — which is kind of ironic, when you think about it...
  - rramadass 6y ago
    I believe you are being facetious here. This is a forum for stimulating discussions and exchange of ideas. The fact that you only "see vague statements and handwaving" is more a reflection of one's knowledge bank (or lack thereof) than any shortcoming of the subject or its proponents. By definition this is a complicated and difficult subject and when a computer science pioneer and great like Edsger Dijkstra says something, you pay attention and think about it :-) PS: "Excel" can be thought of as a program generator which specifies a metalanguage (i.e. a "grammar") for a set of DSLs (i.e. Spreadsheet formulas). A little Googling brought up "ViTSL/Gencel"(https://web.engr.oregonstate.edu/~erwig/Gencel/ https://web.engr.oregonstate.edu/~erwig/Gencel/) and "Classheets"(http://www.jot.fm/issues/issue_2007_10/paper19/index.html http://www.jot.fm/issues/issue_2007_10/paper19/index.html) showing approaches to specifying "correct" Spreadsheets.

by adwn 6y ago

TheOtherHobbes 6y ago

Quite. It's the silliest of silly ideas - not just practically, but conceptually, because real problems don't have hard algorithmic edges. Which is why they're so hard. Don't forget there's a difference between a formal (user) specification and a functional specification. A functional specification says that when you select "Edit -> Cut" the user can expect certain things to happen. A formal specification defines how the symbolic entities involved in implementing the operation should operate. This isn't too hard for "Edit -> Cut", but it's not tractable at all for "Translate this poetry into another language without mistakes or ambiguities." So in fact he's just as guilty of resorting to metaphor as anyone else in computing. Only in this case the metaphor is the algorithmic perfection and consistency of a mathematical proof. This is fine in the classroom and in certain applications where formal methods can help, but not so much in the average developer room. It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets. But I expect he'd have dismissed that idea as too dangerously novel.

rramadass 6y ago
>It also highlights that ultimately computers aren't about manipulating symbols, but about manipulating conceptual metaphors represented by symbol sets. Not quite. Computers only deal with Symbolic Logic via Formal Systems. The mapping of those to a Domain of Discourse is the job of the Programmer.

rramadass 6y ago

Here is Dijkstra himself answering the charge via EWD288 - "Concern for Correctness as a Guiding Principle for Program Composition". Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. In the step-wise approach it is suggested that even in the case of a well-defined task, certain aspects of the given problem statement are ignored at the beginning. This means that the programmer does not regard the given task as an isolated thing to be done, but is invited to view the task as a member of a whole family; he is invited to make the suitable generalizations of the given problem statement. By successively adding more detail in the lower levels he eventually pins his program down to a solution for the given problem. You can also find some relevant discussion (including my posts) at https://news.ycombinator.com/item?id=24942671 https://news.ycombinator.com/item?id=24942671 The point is that by using a top-down and step-wise refinement methodology one can show "correctness" at whatever level of granularity is acceptable.

adwn 6y ago
What would a coarse-granular specification for Excel look like? How would you prove correctness against such a spec? Examples, please. In these discussions, I only ever see vague statements and handwaving by formal verification proponents — which is kind of ironic, when you think about it...
- rramadass 6y ago
  I believe you are being facetious here. This is a forum for stimulating discussions and exchange of ideas. The fact that you only "see vague statements and handwaving" is more a reflection of one's knowledge bank (or lack thereof) than any shortcoming of the subject or its proponents. By definition this is a complicated and difficult subject and when a computer science pioneer and great like Edsger Dijkstra says something, you pay attention and think about it :-) PS: "Excel" can be thought of as a program generator which specifies a metalanguage (i.e. a "grammar") for a set of DSLs (i.e. Spreadsheet formulas). A little Googling brought up "ViTSL/Gencel"(https://web.engr.oregonstate.edu/~erwig/Gencel/ https://web.engr.oregonstate.edu/~erwig/Gencel/) and "Classheets"(http://www.jot.fm/issues/issue_2007_10/paper19/index.html http://www.jot.fm/issues/issue_2007_10/paper19/index.html) showing approaches to specifying "correct" Spreadsheets.