3 ms·

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

>> 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 '='.

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 '='.