5 ms·

I'm a huge fan of Dijkstra, for obvious reasons, and I won't trot out the usual argument that "he's living in an ivory tower" or that "formal analysis is imposs

by hvs 17y ago

I'm a huge fan of Dijkstra, for obvious reasons, and I won't trot out the usual argument that "he's living in an ivory tower" or that "formal analysis is impossible in large applications", but his attitude towards "Software Engineering" does become grating after reading many of his articles. One of the primary reasons that formal analysis is not widely used in software development today (besides the fact that it is often very difficult) is not due to the stupidity or laziness of "software engineers". It is due to the radical failing of computer scientists to both effectively teach the concept, and to develop tools to make it practical. On top of that, the widely used languages in the industry today are just now beginning to allow for the type of high-level formal analysis that Dijkstra promotes. Functional languages are finally starting to make inroads into the industry in the form of Haskell, F#, Erlang; and even imperative languages such as C# are adopting functional attributes. But we are still a long way from the regular use of formal analysis (if it ever actually occurs) because the universities are not providing much, if any, guidance in this area to the industry. Formal analysis is a very hard -- maybe impossible -- problem for anything but toy applications. And I think it is an worthy goal to attempt to achieve, but it will not be well-served by denigrating the work of the many dedicated and intelligent "Software Engineers".

spitfire 17y ago
Formal analysis is a fact of life in many industries. Aviation, rail/transportation, medical systems and some power systems. All these industries have one thing in common - a lot of money to throw around. So the technology and techniques are there, they just have to be brought down to the masses. There are signs of that happening, it just may take more time than you expect.
- hvs 17y ago
  I don't think it'll take more time than I expect, but I take your point. Like I said, I think formal analysis of software development is a laudable goal that should be pursued. But in many ways, software is so much more complex than other engineering fields that it becomes increasingly difficult if the development is not carefully controlled (something that Dijkstra is a big believer in). I know that Dijkstra recognizes that it is not an easy problem to solve, and that he feels that computer scientists have not adequately researched this area. My main point was more about his general attitude to computer engineers than to his actual point. He addresses this well in this EWD Manuscript: http://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1304.html http://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1304...
  - spitfire 17y ago
    I agree with you entirely. A huge problem is in mindset and culture. I've mentioned formal methods here on HN before and been essentially shouted down. Which seems odd considering the hacker-above-the-commoners ethos HN wears on its sleeve. But I digress, I think in the next few years as functional languages become more mainstream we'll see a huge uptake in formal methods. Not end to end mind you, but of the low level proover type tools. Formal project planning and design languages still take too much training to be widely accepted. Can you imaging a ruby hacker analyzing and writing up his code in Z language before they code? Neither can I. But any amount of progress on this front is a good thing.
    - 10ren 17y ago
      BTW: it's not so odd if you think of a hacker as an expert tinkerer. Tinkering is the opposite of upfront design.
- glhaynes 17y ago
  "All these industries have one thing in common - a lot of money to throw around." That "lots of money" is the one thing these industries (that disproportionately involve critical and hazardous scenarios) have in common was a joke, right?
gaius 17y ago
I dunno, Dijkstra always struck me as a throwback to this "high priesthood" era of computing, where The Computer sat serenely in its pristine temple, attended by the brethren in their white coats, sneering at the users who humbly submitted their programs. Well guess what, the democratization of computing happened, no putting that genie back in the bottle. Now millions of people use computers and so what if most of them are writing VBA macros and PHP pages and Perl scripts, their lives are materially improved by it, society is wealthier for it, and Dijkstra is nowhere. GOTO GOTO GOTO

by hvs 17y ago

spitfire 17y ago

Formal analysis is a fact of life in many industries. Aviation, rail/transportation, medical systems and some power systems. All these industries have one thing in common - a lot of money to throw around. So the technology and techniques are there, they just have to be brought down to the masses. There are signs of that happening, it just may take more time than you expect.

hvs 17y ago
I don't think it'll take more time than I expect, but I take your point. Like I said, I think formal analysis of software development is a laudable goal that should be pursued. But in many ways, software is so much more complex than other engineering fields that it becomes increasingly difficult if the development is not carefully controlled (something that Dijkstra is a big believer in). I know that Dijkstra recognizes that it is not an easy problem to solve, and that he feels that computer scientists have not adequately researched this area. My main point was more about his general attitude to computer engineers than to his actual point. He addresses this well in this EWD Manuscript: http://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1304.html http://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD1304...
- spitfire 17y ago
  I agree with you entirely. A huge problem is in mindset and culture. I've mentioned formal methods here on HN before and been essentially shouted down. Which seems odd considering the hacker-above-the-commoners ethos HN wears on its sleeve. But I digress, I think in the next few years as functional languages become more mainstream we'll see a huge uptake in formal methods. Not end to end mind you, but of the low level proover type tools. Formal project planning and design languages still take too much training to be widely accepted. Can you imaging a ruby hacker analyzing and writing up his code in Z language before they code? Neither can I. But any amount of progress on this front is a good thing.
  - 10ren 17y ago
    BTW: it's not so odd if you think of a hacker as an expert tinkerer. Tinkering is the opposite of upfront design.
glhaynes 17y ago
"All these industries have one thing in common - a lot of money to throw around." That "lots of money" is the one thing these industries (that disproportionately involve critical and hazardous scenarios) have in common was a joke, right?

gaius 17y ago

I dunno, Dijkstra always struck me as a throwback to this "high priesthood" era of computing, where The Computer sat serenely in its pristine temple, attended by the brethren in their white coats, sneering at the users who humbly submitted their programs. Well guess what, the democratization of computing happened, no putting that genie back in the bottle. Now millions of people use computers and so what if most of them are writing VBA macros and PHP pages and Perl scripts, their lives are materially improved by it, society is wealthier for it, and Dijkstra is nowhere. GOTO GOTO GOTO