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 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.)