11 ms·

A Bridge Too Far: E.W. Dijkstra and Logic

127 points by akkartik 8y ago

zimablue 8y ago
I'm fighting through a book on formal logic at the moment, I never did a computer science degree, is it on the syllabus? It feels like this should have been the first thing I ever studied. I kind of got to it in reverse, data shuffling => everything looks like sql/pandas => everything is relational logic (read about minikanren, datalog, prolog) => lots of things are a surprisingly thin layer over formal logic. I haven't explored the idea but I read somewhere that type systems are close to unification (rust's typesystem is apparently very close ??). Interesting to see this article and realise that Dijkstra (God) was interested in logic too. Has anyone explored the idea that you write your program largely in logic, and that's your spec/typesystem, then you write the performance-relevant parts in a more procedural language, with either generative tests or some kind of proof system showing their equivalence?
- auggierose 8y ago
  Yeah, that's the basic idea of refinement based program verification. An example of that is: https://github.com/seL4/l4v https://github.com/seL4/l4v There are many programs which can be nicely specified with logic, and which could thus be treated this way. That we haven't build up the infrastructure yet to do this cheaply and routinely for those kinds of programs / libraries has various reasons. For example software engineers never doing a computer science degree ;-)
- YorkshireSeason 8y ago
  > is [logic] on the syllabus? It used to be, but these days, most normal universities have de-mathematised their core CS curriculum, and logic is rarely taught in any depth. If you are lucky it's a short few lectures on some introductory mathematics-for-computer-science Year 1 lecture. > this should have been the first thing I ever studied. In my experience as a CS prof at university, teaching logic at the start of a CS course will baffle 99% of students, and they will not see the point. At the same time, the top 1% love it. Note that as of January 2019, most programming jobs, including top paying FAANG jobs, don't require a substantial grounding in logic. Note that logic is deeply engrained in human thinking, we intuitively understand the meaning of terms like not, and, or, exists etc from early childhood on. The Kantian hypothesis here is that logic is part of the very fabric of our preception. So on some level, we don't need to learn logic as adults. What a logic course does it, tell us how to formalise logic. Moreover, by the Curry-Howard correspondence [4], (constructive) logic and programming are essentially the same thing, so one might argue that a computer science degree is basically a long logic course, but using a novel approach to formalising logic. > type systems are close to unification Yes, in the sense that type inference does unification. The most famous paper on type inference [1] is explicitly based on Robinson's famous unification algorithm [2]. User "dkarapetyan" in [3] even quipped: "Any sufficiently advanced type system is an ad-hoc re-implementation of Prolog. Once you have unification and backtracking you basically have Prolog and can implement whatever Turing machine you want with the type system." Relatedly, compilers for languages with advanced typing systems are sometimes quite slow (e.g. the old Scala compiler), and the cost of unification plays a big role here. As an aside, I recommend implementing the core type-inference algorithm in [1] for a toy language. It's simple, only ~100 LoCs in a high-level language, but it will really help you understand typing systems, and hence modern programming languages. Few things amplify your understanding of programming languages so much, for so little effort. > proof system showing their equivalence? Proving equivalence between programs is not computable (by easy reduction to the halting problem), and infeasibly expensive to do manually for non-trivial programs. Barring unexpected breakthroughs in algorithms (e.g. a constructive proof that P=NP), this is likely not to change in the next decade or two. [1] L. Damas, R. Milner, Principal type-schemes for functional programs. [2] J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle. [3] https://news.ycombinator.com/item?id=13843288 https://news.ycombinator.com/item?id=13843288 [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
  - claudiawerner 8y ago
    >So on some level, we don't need to learn logic as adults. What a logic course does it, tell us how to formalise logic. Unless it's a course in dialectical logic, or actually any other non-classical logic.
    - YorkshireSeason 8y ago
      I'm not sure what you mean. All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classical logics are explained in is traditional first-order logic, see e.g. [1]. I don't know what "dialectical logic" logic is. [1] Graham Priest, An Introduction to Non-Classical Logic
      - claudiawerner 8y ago
        Dialectical logic is a name given to describe the non-formal method apparent in Hegel's work, in which two opposing poles confront each other and progress towards a positive outcome. https://plato.stanford.edu/entries/hegel-dialectics/ https://plato.stanford.edu/entries/hegel-dialectics/
        YorkshireSeason 8y ago
        The word logic has seen a marked shift (restriction) since Hegel's times: what Hegel meant by logic is no longer what we mean today by the term.
        claudiawerner 8y ago
        I'd question whether the people who talk about logic in analytic philosophy departments and mathematics have a monopoly on the usage of an ancient term and concept which has found immense value in non-formal contexts too.
        8y ago
- deleted 8y ago
  [deleted]
- arethuza 8y ago
  I'm pretty sure we did propositional and predicate logic in first year - UK CS course in the 1980s. Programming proving and synthesis was second year stuff, of a four year course.
- MaysonL 8y ago
  Back in high school (early '60s), I studied Suzanne Langer's Introduction to Symbolic Logic, and the fluency that gave me in Boolean algebra and bit-twiddling had me in good shape for many years.
stiff 8y ago
There are some good lecture videos with Dijkstra online that give a better introduction to his way of thinking than anything he wrote: "Reasoning about programs": https://www.youtube.com/watch?v=GX3URhx6i2E https://www.youtube.com/watch?v=GX3URhx6i2E "The power of counting arguments": https://www.youtube.com/watch?v=0kXjl2e6qD0 https://www.youtube.com/watch?v=0kXjl2e6qD0 "Structured programming": https://www.youtube.com/watch?v=72RA6Dc7rMQ https://www.youtube.com/watch?v=72RA6Dc7rMQ "NU lecture": https://www.youtube.com/watch?v=qNCAFcAbSTg https://www.youtube.com/watch?v=qNCAFcAbSTg
evertheylen 8y ago
For those interested in Dijkstra, this website has a lot to offer: http://www.dijkstrascry.com/ http://www.dijkstrascry.com/ I also followed some lectures given by the guy that runs that website. Apparently Dijkstra was not an easy person to get along with, there are stories of him being bored during some lecture, walking to the front, and laying down for a nap. (Sorry I can't provide a source, it's basically a rumour among academic staff here in Belgium).
- duckerude 8y ago
  > David Gries (Cornell University) was one of the recipients of "on-line" coaching during a lecture: > My own experience with lecturing before Edsger took place in Marktoberdorf. It rests on the fact that in some languages (notably Fortran), the equality symbol and the assignment symbol are the same, and many people say "x equals e" when they mean "store the value of e in x," or "x becomes e." > I was lecturing along, when I said "x equals e" meaning an assignment of e to x. From the back of the room came a loud "becomes," and then a stunned silence. Finally, I gathered my wits and said, "Thank you, Edsger, for correcting me. If I make the same mistake again, stop me." Twenty minutes later, I made the same mistake, and again from the back of the room came "becomes" "Thanks, I won't make the mistake again," I said, and to this day I haven't! (https://history.computer.org/pioneers/dijkstra.html https://history.computer.org/pioneers/dijkstra.html)
- kieckerjan 8y ago
  One of my drinking buddies, who has no affinity with computers whatsoever, recently casually remarked how he had often met Dijkstra. Apparently he was friends with one of the Dijkstra kids and used to visit him at their home in Nuenen. "The father was supposed to be some hotshot computer professor." Needless to say, I nearly swooned when he told that. I couldn't help pumping him for details, none of which I feel at liberty to pass on to you, except that he thought Dijkstra was excentric but kind.
  - wsc981 8y ago
    Perhaps not completely related to this topic, but interesting nonetheless, a small picture into Dijkstra's life from Dutch tv (subtitled in English): https://www.youtube.com/watch?v=RCCigccBzIU https://www.youtube.com/watch?v=RCCigccBzIU
amacbride 8y ago
“7.1. Don’t go for homebrew logics D&S is not the only example; in general computer people seem to have a penchant for whipping up homebrew logics. See E.F. Codd’s Relational Calculus [12], an obvious mess.” An interesting perspective, and perhaps technically valid from a purely theoretical perspective; however, the field seems to have found a few practical uses for it: just ask Jim Gray and Mike Stonebraker, among others. (keywords to search: System R, SQL, RDBMS, INGRES, Postgres)
- pjungwir 8y ago
  That line stood out to me too, since relational theory has been such a success. I was surprised that [12] is just Codd's paper "Relational Completeness of Data Base Sublanguages," where he introduces first relational algebra and then relational calculus. I read that paper just last year, and it didn't seem like a mess to me. Perhaps he was thinking of three-valued logic (i.e. NULLs), which came later? I'd like to learn more about how the relational calculus is an obvious mess.
  - AnimalMuppet 8y ago
    EWD has his own idea of the "right" ways to program, think, and do math. If your ideas don't fit in with his approach, then your ideas are obviously garbage (to EWD, and he will not be shy about making his view known), no matter how formally correct or useful they are.
    - pjungwir 8y ago
      Okay, but this is the author's opinion here, not EWD's. It was quite a glib dismissal, and footnoting it seems a bit disingenuous even, hinting to casual readers that there is some substance to his "obvious mess", when really the footnote is just to Codd's own paper. (You find these cunning footnotes everywhere btw.) Did EWD feel the same way about the relational calculus? What are the criticisms? I know plenty of ways SQL doesn't live up to relational theory, but this is about relational theory itself: the paper suggests that there is something unsound about it, and that Codd could have invented something better if he had gotten help from a professional logician.
iamcurious 8y ago
Can someone explain how Dijkstra Predicate Logic differs from mainstream Predicate Logic? The section that is supposed to explain this goes on to say "If you are interested in boolean term logic, look elsewhere." and then mentions something of functions mirroring predicates which is something I don´t recall having trouble with when working through when reading EWDs.
- mcguire 8y ago
  I'm interested in this, too. I don't know what is meant by "Boolean term logic." On the other hand, it reminds me of a comment by EWD discussing the meaning of "1 = 2"; according to him, his mother would say it's meaningless ("not well formed?"), while he, or someone, would say it's simply false.
deleted 8y ago
[deleted]
boshomi 8y ago
The referenced interview: An Interview With Edsger W. Dijkstra by Thomas J. Misa (DOI:http://doi.acm.org/10.1145/1787234.1787249 http://doi.acm.org/10.1145/1787234.1787249) https://cacm.acm.org/magazines/2010/8/96632-an-interview-with-edsger-w-dijkstra/fulltext https://cacm.acm.org/magazines/2010/8/96632-an-interview-wit...

127 points by akkartik 8y ago

I'm fighting through a book on formal logic at the moment, I never did a computer science degree, is it on the syllabus? It feels like this should have been the first thing I ever studied. I kind of got to it in reverse, data shuffling => everything looks like sql/pandas => everything is relational logic (read about minikanren, datalog, prolog) => lots of things are a surprisingly thin layer over formal logic. I haven't explored the idea but I read somewhere that type systems are close to unification (rust's typesystem is apparently very close ??). Interesting to see this article and realise that Dijkstra (God) was interested in logic too. Has anyone explored the idea that you write your program largely in logic, and that's your spec/typesystem, then you write the performance-relevant parts in a more procedural language, with either generative tests or some kind of proof system showing their equivalence?

auggierose 8y ago
Yeah, that's the basic idea of refinement based program verification. An example of that is: https://github.com/seL4/l4v https://github.com/seL4/l4v There are many programs which can be nicely specified with logic, and which could thus be treated this way. That we haven't build up the infrastructure yet to do this cheaply and routinely for those kinds of programs / libraries has various reasons. For example software engineers never doing a computer science degree ;-)
YorkshireSeason 8y ago
> is [logic] on the syllabus? It used to be, but these days, most normal universities have de-mathematised their core CS curriculum, and logic is rarely taught in any depth. If you are lucky it's a short few lectures on some introductory mathematics-for-computer-science Year 1 lecture. > this should have been the first thing I ever studied. In my experience as a CS prof at university, teaching logic at the start of a CS course will baffle 99% of students, and they will not see the point. At the same time, the top 1% love it. Note that as of January 2019, most programming jobs, including top paying FAANG jobs, don't require a substantial grounding in logic. Note that logic is deeply engrained in human thinking, we intuitively understand the meaning of terms like not, and, or, exists etc from early childhood on. The Kantian hypothesis here is that logic is part of the very fabric of our preception. So on some level, we don't need to learn logic as adults. What a logic course does it, tell us how to formalise logic. Moreover, by the Curry-Howard correspondence [4], (constructive) logic and programming are essentially the same thing, so one might argue that a computer science degree is basically a long logic course, but using a novel approach to formalising logic. > type systems are close to unification Yes, in the sense that type inference does unification. The most famous paper on type inference [1] is explicitly based on Robinson's famous unification algorithm [2]. User "dkarapetyan" in [3] even quipped: "Any sufficiently advanced type system is an ad-hoc re-implementation of Prolog. Once you have unification and backtracking you basically have Prolog and can implement whatever Turing machine you want with the type system." Relatedly, compilers for languages with advanced typing systems are sometimes quite slow (e.g. the old Scala compiler), and the cost of unification plays a big role here. As an aside, I recommend implementing the core type-inference algorithm in [1] for a toy language. It's simple, only ~100 LoCs in a high-level language, but it will really help you understand typing systems, and hence modern programming languages. Few things amplify your understanding of programming languages so much, for so little effort. > proof system showing their equivalence? Proving equivalence between programs is not computable (by easy reduction to the halting problem), and infeasibly expensive to do manually for non-trivial programs. Barring unexpected breakthroughs in algorithms (e.g. a constructive proof that P=NP), this is likely not to change in the next decade or two. [1] L. Damas, R. Milner, Principal type-schemes for functional programs. [2] J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle. [3] https://news.ycombinator.com/item?id=13843288 https://news.ycombinator.com/item?id=13843288 [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- claudiawerner 8y ago
  >So on some level, we don't need to learn logic as adults. What a logic course does it, tell us how to formalise logic. Unless it's a course in dialectical logic, or actually any other non-classical logic.
  - YorkshireSeason 8y ago
    I'm not sure what you mean. All formalisations of non-classical logic operate in the framework of first-order logic, in the sense that the informal meta-language in which the non-classical logics are explained in is traditional first-order logic, see e.g. [1]. I don't know what "dialectical logic" logic is. [1] Graham Priest, An Introduction to Non-Classical Logic
    - claudiawerner 8y ago
      Dialectical logic is a name given to describe the non-formal method apparent in Hegel's work, in which two opposing poles confront each other and progress towards a positive outcome. https://plato.stanford.edu/entries/hegel-dialectics/ https://plato.stanford.edu/entries/hegel-dialectics/
      - YorkshireSeason 8y ago
        The word logic has seen a marked shift (restriction) since Hegel's times: what Hegel meant by logic is no longer what we mean today by the term.
        claudiawerner 8y ago
        I'd question whether the people who talk about logic in analytic philosophy departments and mathematics have a monopoly on the usage of an ancient term and concept which has found immense value in non-formal contexts too.
        8y ago
deleted 8y ago
[deleted]
arethuza 8y ago
I'm pretty sure we did propositional and predicate logic in first year - UK CS course in the 1980s. Programming proving and synthesis was second year stuff, of a four year course.
MaysonL 8y ago
Back in high school (early '60s), I studied Suzanne Langer's Introduction to Symbolic Logic, and the fluency that gave me in Boolean algebra and bit-twiddling had me in good shape for many years.

stiff 8y ago

There are some good lecture videos with Dijkstra online that give a better introduction to his way of thinking than anything he wrote: "Reasoning about programs": https://www.youtube.com/watch?v=GX3URhx6i2E https://www.youtube.com/watch?v=GX3URhx6i2E "The power of counting arguments": https://www.youtube.com/watch?v=0kXjl2e6qD0 https://www.youtube.com/watch?v=0kXjl2e6qD0 "Structured programming": https://www.youtube.com/watch?v=72RA6Dc7rMQ https://www.youtube.com/watch?v=72RA6Dc7rMQ "NU lecture": https://www.youtube.com/watch?v=qNCAFcAbSTg https://www.youtube.com/watch?v=qNCAFcAbSTg

evertheylen 8y ago

For those interested in Dijkstra, this website has a lot to offer: http://www.dijkstrascry.com/ http://www.dijkstrascry.com/ I also followed some lectures given by the guy that runs that website. Apparently Dijkstra was not an easy person to get along with, there are stories of him being bored during some lecture, walking to the front, and laying down for a nap. (Sorry I can't provide a source, it's basically a rumour among academic staff here in Belgium).

duckerude 8y ago
> David Gries (Cornell University) was one of the recipients of "on-line" coaching during a lecture: > My own experience with lecturing before Edsger took place in Marktoberdorf. It rests on the fact that in some languages (notably Fortran), the equality symbol and the assignment symbol are the same, and many people say "x equals e" when they mean "store the value of e in x," or "x becomes e." > I was lecturing along, when I said "x equals e" meaning an assignment of e to x. From the back of the room came a loud "becomes," and then a stunned silence. Finally, I gathered my wits and said, "Thank you, Edsger, for correcting me. If I make the same mistake again, stop me." Twenty minutes later, I made the same mistake, and again from the back of the room came "becomes" "Thanks, I won't make the mistake again," I said, and to this day I haven't! (https://history.computer.org/pioneers/dijkstra.html https://history.computer.org/pioneers/dijkstra.html)
kieckerjan 8y ago
One of my drinking buddies, who has no affinity with computers whatsoever, recently casually remarked how he had often met Dijkstra. Apparently he was friends with one of the Dijkstra kids and used to visit him at their home in Nuenen. "The father was supposed to be some hotshot computer professor." Needless to say, I nearly swooned when he told that. I couldn't help pumping him for details, none of which I feel at liberty to pass on to you, except that he thought Dijkstra was excentric but kind.
- wsc981 8y ago
  Perhaps not completely related to this topic, but interesting nonetheless, a small picture into Dijkstra's life from Dutch tv (subtitled in English): https://www.youtube.com/watch?v=RCCigccBzIU https://www.youtube.com/watch?v=RCCigccBzIU

amacbride 8y ago

“7.1. Don’t go for homebrew logics D&S is not the only example; in general computer people seem to have a penchant for whipping up homebrew logics. See E.F. Codd’s Relational Calculus [12], an obvious mess.” An interesting perspective, and perhaps technically valid from a purely theoretical perspective; however, the field seems to have found a few practical uses for it: just ask Jim Gray and Mike Stonebraker, among others. (keywords to search: System R, SQL, RDBMS, INGRES, Postgres)

pjungwir 8y ago
That line stood out to me too, since relational theory has been such a success. I was surprised that [12] is just Codd's paper "Relational Completeness of Data Base Sublanguages," where he introduces first relational algebra and then relational calculus. I read that paper just last year, and it didn't seem like a mess to me. Perhaps he was thinking of three-valued logic (i.e. NULLs), which came later? I'd like to learn more about how the relational calculus is an obvious mess.
- AnimalMuppet 8y ago
  EWD has his own idea of the "right" ways to program, think, and do math. If your ideas don't fit in with his approach, then your ideas are obviously garbage (to EWD, and he will not be shy about making his view known), no matter how formally correct or useful they are.
  - pjungwir 8y ago
    Okay, but this is the author's opinion here, not EWD's. It was quite a glib dismissal, and footnoting it seems a bit disingenuous even, hinting to casual readers that there is some substance to his "obvious mess", when really the footnote is just to Codd's own paper. (You find these cunning footnotes everywhere btw.) Did EWD feel the same way about the relational calculus? What are the criticisms? I know plenty of ways SQL doesn't live up to relational theory, but this is about relational theory itself: the paper suggests that there is something unsound about it, and that Codd could have invented something better if he had gotten help from a professional logician.

iamcurious 8y ago

Can someone explain how Dijkstra Predicate Logic differs from mainstream Predicate Logic? The section that is supposed to explain this goes on to say "If you are interested in boolean term logic, look elsewhere." and then mentions something of functions mirroring predicates which is something I don´t recall having trouble with when working through when reading EWDs.

mcguire 8y ago
I'm interested in this, too. I don't know what is meant by "Boolean term logic." On the other hand, it reminds me of a comment by EWD discussing the meaning of "1 = 2"; according to him, his mother would say it's meaningless ("not well formed?"), while he, or someone, would say it's simply false.

deleted 8y ago

[deleted]

boshomi 8y ago

The referenced interview: An Interview With Edsger W. Dijkstra by Thomas J. Misa (DOI:http://doi.acm.org/10.1145/1787234.1787249 http://doi.acm.org/10.1145/1787234.1787249) https://cacm.acm.org/magazines/2010/8/96632-an-interview-with-edsger-w-dijkstra/fulltext https://cacm.acm.org/magazines/2010/8/96632-an-interview-wit...