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.
> 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.
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.
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_simpl...
[2] https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem