![]() | This article was nominated for deletion on August 8, 2006. The result of the discussion was keep. |
![]() | This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | |||||||||||||||||
|
As requested and as an actual participant in the 1990 debate On the Cruelty ( http://catless.ncl.ac.uk/Risks/11.86.html#subj1) I have expanded this stub. --Edward G. Nilges
This article needs rewriting remove the gobbledegook and put whats left into plain words 82.38.97.206 09:11, 13 January 2006 (UTC)mikeL
What's with all the irrelevant references to women? Was this an actual part of the original debate, or is it just editorialising on the part of the writer? -- 221.249.13.34 04:54, 8 Nov 2004 (UTC)
Computer programs are written primarily for real-world purposes. Mathematical proof or freedom from bugs is far down on the list of priorities, and rightly so.
Microsoft does not need formal proof to market and sell a product. Producing a formal proof would be a massive effort, costing more money that could be recovered from the value-added the proof might produce.
Even if they wanted to, no sufficiently-rigorous definitions are ever produced for large programs to drive such a formal proof.
Formal proof of correctness is the essence of Ivory Tower.
Only someone who has never worked overtime against a ship date, and never dealt with fuzzy requirements, and never fended off a customer so eager for a product they would take a version known to be buggy, would fail to see, or de-emphasize, the real-world counterpoints to thus exalting formal proof. = unkown = -- Williamv1138
The position expressed in e.g. Kernighan and Plauger's The Elements of Programming Style has an interestingly equivocal relationship to Dijkstra's. It's far from academic and not concerned with proving the correctness of programs, but they shared Dijkstra's concern with structured programming somewhat before it became ubiquitous, and they have some sarcastic things to say about cleverness and "efficiency" ("One hopes that the increased efficiency of the program will help to compensate for giving everyone a 10% discount." "Presumably this means that it is vital to get the wrong answers quickly.") DanielCristofani 09:42, 17 December 2005 (UTC)
I did a major rewrite to remove editorializing and make the flow sound more encyclopedia, rather than an essay written by a friend or colleague.
I moved some biographical text to Talk:Edsger Dijkstra, since it seemed more appropriate for that article, if it's going to be anywhere.
I was unable to resolve one issue. Consider the following quotes:
You certainly don't need to know the details of how a program is actually compiled and run in order to be able to model it mathematically and make formal statements about it. I'm not sure the debate over how much detail students should be taught is related to the debate over formal correctness. Was the compiler example or anything like it something Dijkstra used in his paper? If not, it might not be relevant to the topic.
At MIT, at least, computer science majors are taught everything from how the EM fields inside transitors give rise to their electrical properties, to how they are assembled into logic gates and chips, to how the kernel and compiler work, to high-level artificial intelligence techniques. The introductory CS class includes the construction of a Lisp interpreter in Lisp, which is indeed rather mind-warping and somewhat pointless except for its educational side-effects. (But why else would you be in college if not to learn? Wait...don't answer that.) I can't really evaluate the scope of the curriculum at other schools, though, and that only needs to be in the article if this is relevant to assessing the legacy of this paper.
-- Beland 01:42, 2 May 2006 (UTC)
I removed "Not true about the University of Warsaw" because it wasn't referenced or explained. Also, I'm not certain that listing schools that follow Dijkstra is a good idea. If there are schools that follow Dijkstra, we can weaken the wording ("most schools don't...") and reference some curriculum/course explanation pages that use Dijkstra's methods. -- JamesBrownJr ( talk) 22:53, 7 August 2009 (UTC)
From the article:
"Until the end of his life, Dijkstra maintained that the central challenges of computing hadn’t been met to his satisfaction, due to an insufficient emphasis on program correctness (though not obviating other requirements, such as maintainability and efficiency)."
The phrase "until the end of his life" is problematic: one might reasonably infer that Dijkstra changed his opinion at the end of his life, shortly before death.
I think this is probably not the intended case -- it's more likely, in my mind, that Dijkstra did not change his opinion -- in which case, the phrase should read "throughout his adult life," or words to that effect.
If you know the facts of the matter, please update the article as appropriate.
![]() | This article was nominated for deletion on August 8, 2006. The result of the discussion was keep. |
![]() | This article is rated Start-class on Wikipedia's
content assessment scale. It is of interest to the following WikiProjects: | |||||||||||||||||
|
As requested and as an actual participant in the 1990 debate On the Cruelty ( http://catless.ncl.ac.uk/Risks/11.86.html#subj1) I have expanded this stub. --Edward G. Nilges
This article needs rewriting remove the gobbledegook and put whats left into plain words 82.38.97.206 09:11, 13 January 2006 (UTC)mikeL
What's with all the irrelevant references to women? Was this an actual part of the original debate, or is it just editorialising on the part of the writer? -- 221.249.13.34 04:54, 8 Nov 2004 (UTC)
Computer programs are written primarily for real-world purposes. Mathematical proof or freedom from bugs is far down on the list of priorities, and rightly so.
Microsoft does not need formal proof to market and sell a product. Producing a formal proof would be a massive effort, costing more money that could be recovered from the value-added the proof might produce.
Even if they wanted to, no sufficiently-rigorous definitions are ever produced for large programs to drive such a formal proof.
Formal proof of correctness is the essence of Ivory Tower.
Only someone who has never worked overtime against a ship date, and never dealt with fuzzy requirements, and never fended off a customer so eager for a product they would take a version known to be buggy, would fail to see, or de-emphasize, the real-world counterpoints to thus exalting formal proof. = unkown = -- Williamv1138
The position expressed in e.g. Kernighan and Plauger's The Elements of Programming Style has an interestingly equivocal relationship to Dijkstra's. It's far from academic and not concerned with proving the correctness of programs, but they shared Dijkstra's concern with structured programming somewhat before it became ubiquitous, and they have some sarcastic things to say about cleverness and "efficiency" ("One hopes that the increased efficiency of the program will help to compensate for giving everyone a 10% discount." "Presumably this means that it is vital to get the wrong answers quickly.") DanielCristofani 09:42, 17 December 2005 (UTC)
I did a major rewrite to remove editorializing and make the flow sound more encyclopedia, rather than an essay written by a friend or colleague.
I moved some biographical text to Talk:Edsger Dijkstra, since it seemed more appropriate for that article, if it's going to be anywhere.
I was unable to resolve one issue. Consider the following quotes:
You certainly don't need to know the details of how a program is actually compiled and run in order to be able to model it mathematically and make formal statements about it. I'm not sure the debate over how much detail students should be taught is related to the debate over formal correctness. Was the compiler example or anything like it something Dijkstra used in his paper? If not, it might not be relevant to the topic.
At MIT, at least, computer science majors are taught everything from how the EM fields inside transitors give rise to their electrical properties, to how they are assembled into logic gates and chips, to how the kernel and compiler work, to high-level artificial intelligence techniques. The introductory CS class includes the construction of a Lisp interpreter in Lisp, which is indeed rather mind-warping and somewhat pointless except for its educational side-effects. (But why else would you be in college if not to learn? Wait...don't answer that.) I can't really evaluate the scope of the curriculum at other schools, though, and that only needs to be in the article if this is relevant to assessing the legacy of this paper.
-- Beland 01:42, 2 May 2006 (UTC)
I removed "Not true about the University of Warsaw" because it wasn't referenced or explained. Also, I'm not certain that listing schools that follow Dijkstra is a good idea. If there are schools that follow Dijkstra, we can weaken the wording ("most schools don't...") and reference some curriculum/course explanation pages that use Dijkstra's methods. -- JamesBrownJr ( talk) 22:53, 7 August 2009 (UTC)
From the article:
"Until the end of his life, Dijkstra maintained that the central challenges of computing hadn’t been met to his satisfaction, due to an insufficient emphasis on program correctness (though not obviating other requirements, such as maintainability and efficiency)."
The phrase "until the end of his life" is problematic: one might reasonably infer that Dijkstra changed his opinion at the end of his life, shortly before death.
I think this is probably not the intended case -- it's more likely, in my mind, that Dijkstra did not change his opinion -- in which case, the phrase should read "throughout his adult life," or words to that effect.
If you know the facts of the matter, please update the article as appropriate.