4 ms·

Reading up on the history of mathematics really makes that clear as shown in https://www.goodreads.com/book/show/1098132.Thomas_Harriot_s_Artis_Analyticae_Prax

Reading up on the history of mathematics really makes that clear as shown in https://www.goodreads.com/book/show/1098132.Thomas_Harriot_s_Artis_Analyticae_Praxis https://www.goodreads.com/book/show/1098132.Thomas_Harriot_s... (ob. discl., I did the typesetting for that) It shows at least one lengthy and quite wordy example of how an equation would have been stated, then contrasts it in the "new" symbolic representation (this was one of the first major works to make use of Robert Recorde's development of the equals sign).

tim333 2y ago
Although if you look at most maths textbooks or papers there's a fair bit of English waffle per equation. I guess both have their place.
- dmoy 2y ago
  People definitely could stand to write a lot more comments in their code. And like... yea, textbook style prose, not just re-stating the code in slightly less logical wording.
  - WillAdams 2y ago
    Welcome to the world of advocating for Literate Programming: http://literateprogramming.com/ http://literateprogramming.com/
  - hackable_sand 2y ago
    Yes exactly. Or like signposts on a road. "You came from these few places, you might go to these few places, watch out for these bugbears if you go down that one path."
- sabas123 2y ago
  As somebody that occasionally studies pure math books those can be very, very light on regular English.
  - Jensson 2y ago
    That makes them much easier to read though, its so hard to find a specific statement in English compared to math notation since its easier to find a specific symbol than a specific word.
- cratermoon 2y ago
  Yes, plain language text to support and translate symbology to concepts facilitates initial comprehension. It's like two ends of a connection negotiating protocols: once agreed upon, communication proceeds using only symbols.
- whatevertrevor 2y ago
  Textbooks aren't just communicating theorems and proofs (which are often just written in formal symbolic language), but also the language required to teach these concepts, why these are important, how these could be used and sometimes even the story behind the discovery of fields. So this is far from an accurate comparison.
  - School-Cotton 2y ago
    Theorems and proofs are almost never written in formal symbolic language.
    - codebje 2y ago
      My experience in reading computer science papers is almost exactly the opposite of yours: theorems are almost always written in formal symbolic language. Proofs vary more, from brief prose sketching a simple proof to critical components of proofs given symbolically with prose tying it together. (Uncommonly, some papers - mostly those related to type theory - go so far as to reference hundreds of lines of machine verified symbolic proofs.)
      - School-Cotton 2y ago
        Can you give an example of the type of theorem or proof you're talking about?
        codebje 2y ago
        Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation: https://scholar.google.com/scholar?&q=Hinze%2C%20R.%2C%20Paterson%2C%20R.%3A%20Derivation%20of%20a%20typed%20functional%20LR%20parser%20%282003%29 Here's one for the semantics of the Cedille functional language core in which proofs are given as key components in symbolic language with prose to to tie them together; all theorems, lemmas, etc are given symbolically. https://arxiv.org/abs/1806.04709 And here's one introducing dependent intersection types (as used in Cedille) which references formal machine-checked proofs and only provides a sketch of the proof result in prose: https://doi.org/10.1109/LICS.2003.1210048 (For the latter, actually finding the machine checked proof might be tricky: I didn't see it overtly cited and I didn't go looking).

tim333 2y ago

Although if you look at most maths textbooks or papers there's a fair bit of English waffle per equation. I guess both have their place.

dmoy 2y ago
People definitely could stand to write a lot more comments in their code. And like... yea, textbook style prose, not just re-stating the code in slightly less logical wording.
- WillAdams 2y ago
  Welcome to the world of advocating for Literate Programming: http://literateprogramming.com/ http://literateprogramming.com/
- hackable_sand 2y ago
  Yes exactly. Or like signposts on a road. "You came from these few places, you might go to these few places, watch out for these bugbears if you go down that one path."
sabas123 2y ago
As somebody that occasionally studies pure math books those can be very, very light on regular English.
- Jensson 2y ago
  That makes them much easier to read though, its so hard to find a specific statement in English compared to math notation since its easier to find a specific symbol than a specific word.
cratermoon 2y ago
Yes, plain language text to support and translate symbology to concepts facilitates initial comprehension. It's like two ends of a connection negotiating protocols: once agreed upon, communication proceeds using only symbols.
whatevertrevor 2y ago
Textbooks aren't just communicating theorems and proofs (which are often just written in formal symbolic language), but also the language required to teach these concepts, why these are important, how these could be used and sometimes even the story behind the discovery of fields. So this is far from an accurate comparison.
- School-Cotton 2y ago
  Theorems and proofs are almost never written in formal symbolic language.
  - codebje 2y ago
    My experience in reading computer science papers is almost exactly the opposite of yours: theorems are almost always written in formal symbolic language. Proofs vary more, from brief prose sketching a simple proof to critical components of proofs given symbolically with prose tying it together. (Uncommonly, some papers - mostly those related to type theory - go so far as to reference hundreds of lines of machine verified symbolic proofs.)
    - School-Cotton 2y ago
      Can you give an example of the type of theorem or proof you're talking about?
      - codebje 2y ago
        Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation: https://scholar.google.com/scholar?&q=Hinze%2C%20R.%2C%20Paterson%2C%20R.%3A%20Derivation%20of%20a%20typed%20functional%20LR%20parser%20%282003%29 Here's one for the semantics of the Cedille functional language core in which proofs are given as key components in symbolic language with prose to to tie them together; all theorems, lemmas, etc are given symbolically. https://arxiv.org/abs/1806.04709 And here's one introducing dependent intersection types (as used in Cedille) which references formal machine-checked proofs and only provides a sketch of the proof result in prose: https://doi.org/10.1109/LICS.2003.1210048 (For the latter, actually finding the machine checked proof might be tricky: I didn't see it overtly cited and I didn't go looking).