Recently found this paper, entitled “On the Cruelty of Really Teaching Computer Science” by Dijkstra (plaintext transcription here). It outlines ways in which computer programming had failed to (and still has) actually jump across the transformative-insight gap that led to the creation of the programmable computer. Probably relevant to many of this crowd, and very reminiscent of some common thoughts I’ve seen here related to AI design.
In the same place I found this paper discussed, there was mention of this site, which was recommended as teaching computer science in a way implementing Dijkstra’s suggestions and this textbook, similarly. I can’t vouch for them personally yet, but this might be an appropriate addition to the big list of textbooks.
Dijkstra’s ideas may be relevant to safety-critical domains (at least to some extent) but the article is flagrantly ignoring cost-benefit tradeoffs. Empirically we see that (manual) proof-oriented programming remains a small niche while test-driven programming has been very successful.
He’s certainly not ignoring cost-benefit tradeoffs. He acknowledges this as a perceived weak point, and claims that, when practiced properly, the tradeoff is illusory. (I rate this unlikely but possible, around 2% that it’s purely true and another ~20% that the cost increase is greatly exaggerated.)
I’m pretty sure Dijkstra would argue (and I’m inclined to agree) that proof-oriented programming hasn’t gotten a fair field test, since the field is taught in the test-driven paradigm and his proof-oriented teaching methods were never widely tried. There’s definitely some status quo bias at work; the critical question is whether Dijkstra’s methods would pass the reversal test, and if so how broadly. My intuition suggests “Yes, narrowly with positive outlook”; as we move toward having more and more information on cloud-computing servers and services and social networks, provably-secure computing seems likely to be appealing in increasingly broad applications, particularly when you look at large businesses wanting to reap the benefits of new technologies but very leery of the negative consequences of bugs.
And of course, even in the status quo, these methods still have relevance to anyone looking to make high-risk things like AI.
I’m pretty sure Dijkstra would argue (and I’m inclined to agree) that proof-oriented programming hasn’t gotten a fair field test, since the field is taught in the test-driven paradigm and his proof-oriented teaching methods were never widely tried.
I would be skeptical of this claim, given how diverse the field of software engineering is, and many programmers are both self-taught and mathematically talented, so they would be prone to trying out neat things like proof-oriented programming even if mainstream schools only taught the test-driven paradigm. At the same time, many schools actually focus on teaching computer science instead of software engineering, taking a much more theoretical and mathematical approach than what most programmers will ever actually need. People coming from these backgrounds would also seem to be inclined to try out neat formal methods. (If they pursued an academic career, they could even do so without profitability concerns.)
Dijkstra’s general senitment seems to be that applying existed engineering practices from civil, mechanical, electrical, etc. engineering disciplines to computer science is woefully inadequate. With this, I agree. I also agree that there seems to be some weird set of beliefs in mathematical culture that the human brain is superior to a computer and that no computer could ever do mathematics like a human could (I’ve seen even prominent mathematicians use Godel’s theorem as bogus ‘evidence’ of this).
But the problem is that there doesn’t seem to be a viable alternative to the status quo of software engineering, not at the moment. The only type of radical new thinking that I am aware of is the functional programming approach to things taken by e.g. haskell. But there are a lot of issues there as well. So far, productivity has been far higher using the more traditional way of doing things.
I did some Googling after reading the article and found this book by Dijkstra and Scholten actually showing how a first-order language could be adapted to yield easy and teachable corectness proofs. That is actually amazing! I have a degree in CS and unfortunately I’ve never seen a formal specification system that could actually be implemented and not be just some almost-tautological mathematical logic, like so many systems that exist in the academia. Thanks very much for the link.
If you are interested in this kind of thing, you should check out Dafny. It’s a programming language with Hoare-logic style pre- and postconditions (and the underlying implementation computes weakest preconditions, Dijkstra-style). But what sets it apart is that it is backed by an automatic theorem prover (Z3) which is sufficiently powerful to handle most things that seem trivial to a human. To me Dafny feels like the promise of programming verification research in the 1970s finally came through: you can carry out program verification like you would with pen and paper, without being overwhelmed by finicky algebraic manipulations.
Mathematicians (and Dijkstra qualifies as one) have been bemoaning the lack rigour in undergraduate education for some time now. (Aye, even as early as the French vs. English trigonometry textbook debates of the 1800s.) The United States has a peculiar cultural mismatch between the relative quality of secondary and undergraduate education, which in my mind causes most of the drama. In particular, EWD1036 was written during Dijkstra’s career at UT Austin.
I’d like to know if this phenomena is global, though.
Recently found this paper, entitled “On the Cruelty of Really Teaching Computer Science” by Dijkstra (plaintext transcription here). It outlines ways in which computer programming had failed to (and still has) actually jump across the transformative-insight gap that led to the creation of the programmable computer. Probably relevant to many of this crowd, and very reminiscent of some common thoughts I’ve seen here related to AI design.
In the same place I found this paper discussed, there was mention of this site, which was recommended as teaching computer science in a way implementing Dijkstra’s suggestions and this textbook, similarly. I can’t vouch for them personally yet, but this might be an appropriate addition to the big list of textbooks.
Dijkstra’s ideas may be relevant to safety-critical domains (at least to some extent) but the article is flagrantly ignoring cost-benefit tradeoffs. Empirically we see that (manual) proof-oriented programming remains a small niche while test-driven programming has been very successful.
He’s certainly not ignoring cost-benefit tradeoffs. He acknowledges this as a perceived weak point, and claims that, when practiced properly, the tradeoff is illusory. (I rate this unlikely but possible, around 2% that it’s purely true and another ~20% that the cost increase is greatly exaggerated.)
I’m pretty sure Dijkstra would argue (and I’m inclined to agree) that proof-oriented programming hasn’t gotten a fair field test, since the field is taught in the test-driven paradigm and his proof-oriented teaching methods were never widely tried. There’s definitely some status quo bias at work; the critical question is whether Dijkstra’s methods would pass the reversal test, and if so how broadly. My intuition suggests “Yes, narrowly with positive outlook”; as we move toward having more and more information on cloud-computing servers and services and social networks, provably-secure computing seems likely to be appealing in increasingly broad applications, particularly when you look at large businesses wanting to reap the benefits of new technologies but very leery of the negative consequences of bugs.
And of course, even in the status quo, these methods still have relevance to anyone looking to make high-risk things like AI.
I would be skeptical of this claim, given how diverse the field of software engineering is, and many programmers are both self-taught and mathematically talented, so they would be prone to trying out neat things like proof-oriented programming even if mainstream schools only taught the test-driven paradigm. At the same time, many schools actually focus on teaching computer science instead of software engineering, taking a much more theoretical and mathematical approach than what most programmers will ever actually need. People coming from these backgrounds would also seem to be inclined to try out neat formal methods. (If they pursued an academic career, they could even do so without profitability concerns.)
Dijkstra’s general senitment seems to be that applying existed engineering practices from civil, mechanical, electrical, etc. engineering disciplines to computer science is woefully inadequate. With this, I agree. I also agree that there seems to be some weird set of beliefs in mathematical culture that the human brain is superior to a computer and that no computer could ever do mathematics like a human could (I’ve seen even prominent mathematicians use Godel’s theorem as bogus ‘evidence’ of this).
But the problem is that there doesn’t seem to be a viable alternative to the status quo of software engineering, not at the moment. The only type of radical new thinking that I am aware of is the functional programming approach to things taken by e.g. haskell. But there are a lot of issues there as well. So far, productivity has been far higher using the more traditional way of doing things.
I did some Googling after reading the article and found this book by Dijkstra and Scholten actually showing how a first-order language could be adapted to yield easy and teachable corectness proofs. That is actually amazing! I have a degree in CS and unfortunately I’ve never seen a formal specification system that could actually be implemented and not be just some almost-tautological mathematical logic, like so many systems that exist in the academia. Thanks very much for the link.
If you are interested in this kind of thing, you should check out Dafny. It’s a programming language with Hoare-logic style pre- and postconditions (and the underlying implementation computes weakest preconditions, Dijkstra-style). But what sets it apart is that it is backed by an automatic theorem prover (Z3) which is sufficiently powerful to handle most things that seem trivial to a human. To me Dafny feels like the promise of programming verification research in the 1970s finally came through: you can carry out program verification like you would with pen and paper, without being overwhelmed by finicky algebraic manipulations.
Mathematicians (and Dijkstra qualifies as one) have been bemoaning the lack rigour in undergraduate education for some time now. (Aye, even as early as the French vs. English trigonometry textbook debates of the 1800s.) The United States has a peculiar cultural mismatch between the relative quality of secondary and undergraduate education, which in my mind causes most of the drama. In particular, EWD1036 was written during Dijkstra’s career at UT Austin.
I’d like to know if this phenomena is global, though.