10 ms·

> The programmer is in the unique position that his is the only discipline and profession in which such a gigantic ratio, which totally baffles our imagination,

> The programmer is in the unique position that his is the only discipline and profession in which such a gigantic ratio, which totally baffles our imagination, has to be bridged by a single technology. He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. Compared to that number of semantic levels, the average mathematical theory is almost flat. By evoking the need for deep conceptual hierarchies, the automatic computer confronts us with a radically new intellectual challenge that has no precedent in our history. I am no biographer of Djisktra’s, so is he being unrealistic about programmers here, or does he not have exposure to what a mathematician would consider Mathematics (Wikipedia entry claiming him a mathematician or no)?

wetpaws 2y ago
[dead]
AdieuToLogic 2y ago
>> He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. Compared to that number of semantic levels, the average mathematical theory is almost flat. > ... is he being unrealistic about programmers here, or does he not have exposure to what a mathematician would consider Mathematics? As with any sweeping statement, Dijkstra's assertion is not universally applicable to all programmers. However, for some definition of sufficiently skilled programmer, it is correct if one considers the subset of mathematics applicable to provably correct programs. To wit: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
- chongli 2y ago
  You’ve given a hint of the complexity on the programmer’s side of things but for Dijkstra’s claim to hold we also need to take a look at the mathematician’s. I think most people who are not mathematicians have no idea what they’re working on. Take for example a single theorem: Classification of Finite Simple Groups [1]. This one proof, the work of a hundred mathematicians or so, is tens of thousands of pages long and took half a century to complete. Fermat’s Last Theorem [2] took 358 years to prove and required the development of vast amounts of theory that Fermat himself could scarcely have imagined. [1] https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups https://en.wikipedia.org/wiki/Classification_of_finite_simpl... [2] https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem
  - User23 2y ago
    > This one proof, the work of a hundred mathematicians or so, is tens of thousands of pages long and took half a century to complete. Now compare that to google3 or any other large software. It’s absolutely tiny. A paltry edifice in comparison both in pages and man hours as well as mathematical complexity. Boolean structures get monstrously huge. On the subject of proofs and the verbosity of traditional mathematical methods, this note[1] is interesting. It provides two fun little examples of shorter than normal proofs. It amuses me that just as mathematicians persisted in writing out “is equal to” for decades after Recorde gave us =, there will probably continue to be holdouts who write out “if and only if” instead of using ≡ for many years to come. [1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1073.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD107...
    - Y_Y 2y ago
      I also think "if and only if" is only surpassed by "iff" in badness of notation, though I'd like to put in a good word for classic '='. There's always some implicit inference being made about what kind of equality we're considering, and calling two formulas of logic "equal" if they have the same (truth) value in all cases is reasonable in my book. https://en.wikipedia.org/wiki/Logical_biconditional https://en.wikipedia.org/wiki/Logical_biconditional has some nice comparisons of notation, including a mention that my old friend George Boole also used '='.
csb6 2y ago
I think he was arguing that if programming consists of symbol manipulation and proofs, the task of writing proofs for large programs consists of a lot more symbol manipulation (although probably a lot more tedious in nature) than many proofs written by mathematicians in the past, something made worse by the need to precisely describe each step so that a machine could conceivably execute it instead of being able to skip over proof steps considered “obvious” to a human mathematician. I think he was especially thinking of mathematical logic - he referred to programming as Very Large Scale Application of Logic several times in his writing.
- hughesjj 2y ago
  For the peanut gallery: If you ever want to see what it's like for a mathematician to not hand wave anything away, look at excerpts from Bertrand & Russel in principia mathematics (no, not the newton book). It takes 362 pages (depending on edition) to get to 1+1=2 https://archive.org/details/principia-mathematica_202307/page/362/mode/1up https://archive.org/details/principia-mathematica_202307/pag... Of course, just like real mathematicians, in our everyday work we stand on the shoulders of giants, reuse prior foundational work (I've yet to personally write a bootloader, os, or language+compiler, and include 3p libraries), and then hope that any bugs in our proofs are caught during peer review. Like in math, sometimes peer review for our code ends up being a rubber stamp, or our code/proofs aren't that elegant, or they work for the domain we're using them in but there's latent bugs/logic errors which may cause inconsistencies or require a restriction of domain to properly work (ex code only works with ASCII, or your theorm only works for compact sets). And of course, the similarities aren't a coincidence https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_corresp...
  - black_knight 2y ago
    Note: There are today completely formal systems of proofs which are much more concise than what Russel had. You can now prove 1+1=2 after a few pages of rules (say of Martin-Löf type theory), a couple of definitions (+, 1 and 2) and a very short proof by calculation. In practice, one would use a proof assistant, which is like a programming language, such as Agda. Then it is just the definitions and the proof is just a call to the proof checker to compute and check the result.
Animats 2y ago
> He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. This is not really true. There were complex multilayered systems before computers. In large systems, Western Electric #5 Crossbar was comparable to a large real-time program. General Railway Signal's NX system had the first "intelligent" user interface. But that level of complexity was very rare. Both mechanical design and electronic design are harder than program design. The number of people who did really good mechanism design is tiny. There were only two good typesetting machines, over most of a century - Merganthaler's Linotype and Lanston's Monotype. Everybody else's machine was a dud. In the printing telegraph/Teletype business, Howard Krum and Ed Klienschmidt designed the good ones, and the other twenty or so designs over many decades were much inferior. There were been lathes for centuries, but all modern manual lathes strongly resemble Maudsley's design from 1800. There are far more good programmers than there were good mechanism designers or electronics engineers. Programming is not really that hard by the standards of other complex engineering.
- jayd16 2y ago
  > There are far more good programmers than there were good mechanism designers or electronics engineers. But that doesn't mean a thing. The barrier to entry is much smaller.
  - mock-possum 2y ago
    Yeah if I wanted to just get started with electronics engineering, the easiest cheapest way would be… to use software. Programming / digital engineer bf is lower-stakes than physical stuff.
- User23 2y ago
  > Both mechanical design and electronic design are harder than program design. The number of people who did really good mechanism design is tiny. There were only two good typesetting machines, over most of a century - Merganthaler's Linotype and Lanston's Monotype. That’s a good example and of course it immediately brings to mind TeX, which is an equally monumental if not greater achievement. Certainly there’s no denying that TeX has considerably higher dimensionality than the pre-computerized hot type setting machines. Especially when you include all the ancillary stuff like Metafont. Also recall that Dijkstra was a systems programmer in his industry career. He was well aware of the complexity of the computing hardware of the day—which was cutting edge electronic design. The semaphore wasn’t invented as a cute mathematical trick; he needed it to get hardware interrupts to work properly. Something which THE managed and Unix, among others, never quite did (although it did get to mostly good enough if you don’t mind minefields). > There are far more good programmers than there were good mechanism designers or electronics engineers. Programming is not really that hard by the standards of other complex engineering. Most programmers are incapable of writing a correct binary search, let alone something the size and complexity of TeX with only a handful of relatively minor errors. Programmers capable of that level of intellectual feat are indeed few and far between. I suspect they’re more rare than competent EEs or MEs. Most programmers are more comparable to the guys cleaning the typesetters, not the ones designing them.
User23 2y ago
Dijkstra’s degree was in mathematics. And yes the average mathematical theory is indeed flat compared to a large monolith like google3.
- AnimalMuppet 2y ago
  All right, but the average program is also flat compared to google3. So that argument doesn't prove much.
myworkinisgood 2y ago
Maths has also evolved to be complex now, with the proof of four-color theorem being a computer proof. So, the statement is not as true anymore. But there was a short era when proving that your "static" program was correct was impossible because the number of possible combinations of input approached the size of earth (in terms of how many bits we need to represent). At the same time, almost any single mathematical theorem could be verified by a person to be correct over the course of a couple of years.
- llm_trw 2y ago
  https://celebratio.org/Haken_W/article/794/ https://celebratio.org/Haken_W/article/794/ It was first published in 1976. It is _highly_ unlikely Dijkstra didn't know about it.

wetpaws 2y ago

[dead]

AdieuToLogic 2y ago

>> He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. Compared to that number of semantic levels, the average mathematical theory is almost flat. > ... is he being unrealistic about programmers here, or does he not have exposure to what a mathematician would consider Mathematics? As with any sweeping statement, Dijkstra's assertion is not universally applicable to all programmers. However, for some definition of sufficiently skilled programmer, it is correct if one considers the subset of mathematics applicable to provably correct programs. To wit: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...

chongli 2y ago
You’ve given a hint of the complexity on the programmer’s side of things but for Dijkstra’s claim to hold we also need to take a look at the mathematician’s. I think most people who are not mathematicians have no idea what they’re working on. Take for example a single theorem: Classification of Finite Simple Groups [1]. This one proof, the work of a hundred mathematicians or so, is tens of thousands of pages long and took half a century to complete. Fermat’s Last Theorem [2] took 358 years to prove and required the development of vast amounts of theory that Fermat himself could scarcely have imagined. [1] https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups https://en.wikipedia.org/wiki/Classification_of_finite_simpl... [2] https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem
- User23 2y ago
  > This one proof, the work of a hundred mathematicians or so, is tens of thousands of pages long and took half a century to complete. Now compare that to google3 or any other large software. It’s absolutely tiny. A paltry edifice in comparison both in pages and man hours as well as mathematical complexity. Boolean structures get monstrously huge. On the subject of proofs and the verbosity of traditional mathematical methods, this note[1] is interesting. It provides two fun little examples of shorter than normal proofs. It amuses me that just as mathematicians persisted in writing out “is equal to” for decades after Recorde gave us =, there will probably continue to be holdouts who write out “if and only if” instead of using ≡ for many years to come. [1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1073.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD107...
  - Y_Y 2y ago
    I also think "if and only if" is only surpassed by "iff" in badness of notation, though I'd like to put in a good word for classic '='. There's always some implicit inference being made about what kind of equality we're considering, and calling two formulas of logic "equal" if they have the same (truth) value in all cases is reasonable in my book. https://en.wikipedia.org/wiki/Logical_biconditional https://en.wikipedia.org/wiki/Logical_biconditional has some nice comparisons of notation, including a mention that my old friend George Boole also used '='.

csb6 2y ago

I think he was arguing that if programming consists of symbol manipulation and proofs, the task of writing proofs for large programs consists of a lot more symbol manipulation (although probably a lot more tedious in nature) than many proofs written by mathematicians in the past, something made worse by the need to precisely describe each step so that a machine could conceivably execute it instead of being able to skip over proof steps considered “obvious” to a human mathematician. I think he was especially thinking of mathematical logic - he referred to programming as Very Large Scale Application of Logic several times in his writing.

hughesjj 2y ago
For the peanut gallery: If you ever want to see what it's like for a mathematician to not hand wave anything away, look at excerpts from Bertrand & Russel in principia mathematics (no, not the newton book). It takes 362 pages (depending on edition) to get to 1+1=2 https://archive.org/details/principia-mathematica_202307/page/362/mode/1up https://archive.org/details/principia-mathematica_202307/pag... Of course, just like real mathematicians, in our everyday work we stand on the shoulders of giants, reuse prior foundational work (I've yet to personally write a bootloader, os, or language+compiler, and include 3p libraries), and then hope that any bugs in our proofs are caught during peer review. Like in math, sometimes peer review for our code ends up being a rubber stamp, or our code/proofs aren't that elegant, or they work for the domain we're using them in but there's latent bugs/logic errors which may cause inconsistencies or require a restriction of domain to properly work (ex code only works with ASCII, or your theorm only works for compact sets). And of course, the similarities aren't a coincidence https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_corresp...
- black_knight 2y ago
  Note: There are today completely formal systems of proofs which are much more concise than what Russel had. You can now prove 1+1=2 after a few pages of rules (say of Martin-Löf type theory), a couple of definitions (+, 1 and 2) and a very short proof by calculation. In practice, one would use a proof assistant, which is like a programming language, such as Agda. Then it is just the definitions and the proof is just a call to the proof checker to compute and check the result.

Animats 2y ago

> He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. This is not really true. There were complex multilayered systems before computers. In large systems, Western Electric #5 Crossbar was comparable to a large real-time program. General Railway Signal's NX system had the first "intelligent" user interface. But that level of complexity was very rare. Both mechanical design and electronic design are harder than program design. The number of people who did really good mechanism design is tiny. There were only two good typesetting machines, over most of a century - Merganthaler's Linotype and Lanston's Monotype. Everybody else's machine was a dud. In the printing telegraph/Teletype business, Howard Krum and Ed Klienschmidt designed the good ones, and the other twenty or so designs over many decades were much inferior. There were been lathes for centuries, but all modern manual lathes strongly resemble Maudsley's design from 1800. There are far more good programmers than there were good mechanism designers or electronics engineers. Programming is not really that hard by the standards of other complex engineering.

jayd16 2y ago
> There are far more good programmers than there were good mechanism designers or electronics engineers. But that doesn't mean a thing. The barrier to entry is much smaller.
- mock-possum 2y ago
  Yeah if I wanted to just get started with electronics engineering, the easiest cheapest way would be… to use software. Programming / digital engineer bf is lower-stakes than physical stuff.
User23 2y ago
> Both mechanical design and electronic design are harder than program design. The number of people who did really good mechanism design is tiny. There were only two good typesetting machines, over most of a century - Merganthaler's Linotype and Lanston's Monotype. That’s a good example and of course it immediately brings to mind TeX, which is an equally monumental if not greater achievement. Certainly there’s no denying that TeX has considerably higher dimensionality than the pre-computerized hot type setting machines. Especially when you include all the ancillary stuff like Metafont. Also recall that Dijkstra was a systems programmer in his industry career. He was well aware of the complexity of the computing hardware of the day—which was cutting edge electronic design. The semaphore wasn’t invented as a cute mathematical trick; he needed it to get hardware interrupts to work properly. Something which THE managed and Unix, among others, never quite did (although it did get to mostly good enough if you don’t mind minefields). > There are far more good programmers than there were good mechanism designers or electronics engineers. Programming is not really that hard by the standards of other complex engineering. Most programmers are incapable of writing a correct binary search, let alone something the size and complexity of TeX with only a handful of relatively minor errors. Programmers capable of that level of intellectual feat are indeed few and far between. I suspect they’re more rare than competent EEs or MEs. Most programmers are more comparable to the guys cleaning the typesetters, not the ones designing them.

User23 2y ago

Dijkstra’s degree was in mathematics. And yes the average mathematical theory is indeed flat compared to a large monolith like google3.

AnimalMuppet 2y ago
All right, but the average program is also flat compared to google3. So that argument doesn't prove much.

myworkinisgood 2y ago

Maths has also evolved to be complex now, with the proof of four-color theorem being a computer proof. So, the statement is not as true anymore. But there was a short era when proving that your "static" program was correct was impossible because the number of possible combinations of input approached the size of earth (in terms of how many bits we need to represent). At the same time, almost any single mathematical theorem could be verified by a person to be correct over the course of a couple of years.

llm_trw 2y ago
https://celebratio.org/Haken_W/article/794/ https://celebratio.org/Haken_W/article/794/ It was first published in 1976. It is _highly_ unlikely Dijkstra didn't know about it.