4 ms·

Thanks for reminding me how the rampant abuse of nearly unreadable mathematical notation for things that can be easily expressed in concise natural language con

Thanks for reminding me how the rampant abuse of nearly unreadable mathematical notation for things that can be easily expressed in concise natural language contributed to (voluntarily) shortening my academic career. But more seriously, it's interesting how this produces publications before actual implementations.

jlouis 6y ago
Closer to logic. There is a straightforward rewrite into prolog if you want a program. Or one of the proof assistants. The notation is abused though. Try looking up some of the work by Guy L. Steele in the recent years.
- lazyjones 6y ago
  > Closer to logic. There is a straightforward rewrite into prolog if you want a program. Journal papers usually don't get rewritten into Prolog or fed into proof assistants. They're read by human beings. I've long suspected (and colleagues used to "joke" about it) that excessive use of mathematical notation is just employed to impress and/or confuse peer reviewers into just accepting the paper instead of trying to comprehend it first.
  - jlouis 6y ago
    Well, some journals have demanded proof assistant-level proofs of the work they present. This helps the rigor of the notation a lot since you can't cheat on the proof assistant, and if you confuse it, you are in trouble :) The problem is that getting the notation right is actually quite hard. People write, to the best of their effort, to make the description succinct and understandable. But the notation is pliable, in the same way much mathematics is written: it isn't as rigorous as we would like. Writing the same thing in regular prose is much much harder and there are many more ways things can go wrong. So the state-of-the-art demands formal proof which can be verified by a machine. And it shows in the precision of the notation, which often leaves little to no room for wrong interpretation.
  - Ericson2314 6y ago
    Stop trying to justify your own ignorance. The sequent calculus is great—I am far from an expert and for many papers I can skip the text at first, read the sequents, and then just go back to the prose only if I have specific questions. No prolog conversion needed. As programers, we should be able to read, not just write, formal languages, and appreciate the value of the precision they provide.
    - lazyjones 6y ago
      > Stop trying to justify your own ignorance. I am not ignorant. I tried to rationalize this in the beginning too. It's just hostile towards the reader. > As programers, we should be able to read, not just write, formal languages, and appreciate the value of the precision they provide. We should also be able to see where they are appropriate and where not.
      - Ericson2314 6y ago
        It's not hostile towards this reader (me). It's perfectly appropriate. I would be annoyed if they weren't there.
- adonovan 6y ago
  Just to clarify: Steele has been documenting, not perpetrating, the abuse. See for example https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150_PUBLICATION_ID:5323 https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150...
c-cube 6y ago
If you want to reason about low level compiler optimizations, learn some assembly language. If you want to reason about type systems, learn how to read basic typing rules, it's not complicated. Sometimes planning before implementing is a good thing, or does even language design need to be agile™?
- lazyjones 6y ago
  What is this gibberish? I was fluent in 68k assembly 30 years ago and teaching compiler construction at university 25 years ago. Were you trying to make a point?

jlouis 6y ago

Closer to logic. There is a straightforward rewrite into prolog if you want a program. Or one of the proof assistants. The notation is abused though. Try looking up some of the work by Guy L. Steele in the recent years.

lazyjones 6y ago
> Closer to logic. There is a straightforward rewrite into prolog if you want a program. Journal papers usually don't get rewritten into Prolog or fed into proof assistants. They're read by human beings. I've long suspected (and colleagues used to "joke" about it) that excessive use of mathematical notation is just employed to impress and/or confuse peer reviewers into just accepting the paper instead of trying to comprehend it first.
- jlouis 6y ago
  Well, some journals have demanded proof assistant-level proofs of the work they present. This helps the rigor of the notation a lot since you can't cheat on the proof assistant, and if you confuse it, you are in trouble :) The problem is that getting the notation right is actually quite hard. People write, to the best of their effort, to make the description succinct and understandable. But the notation is pliable, in the same way much mathematics is written: it isn't as rigorous as we would like. Writing the same thing in regular prose is much much harder and there are many more ways things can go wrong. So the state-of-the-art demands formal proof which can be verified by a machine. And it shows in the precision of the notation, which often leaves little to no room for wrong interpretation.
- Ericson2314 6y ago
  Stop trying to justify your own ignorance. The sequent calculus is great—I am far from an expert and for many papers I can skip the text at first, read the sequents, and then just go back to the prose only if I have specific questions. No prolog conversion needed. As programers, we should be able to read, not just write, formal languages, and appreciate the value of the precision they provide.
  - lazyjones 6y ago
    > Stop trying to justify your own ignorance. I am not ignorant. I tried to rationalize this in the beginning too. It's just hostile towards the reader. > As programers, we should be able to read, not just write, formal languages, and appreciate the value of the precision they provide. We should also be able to see where they are appropriate and where not.
    - Ericson2314 6y ago
      It's not hostile towards this reader (me). It's perfectly appropriate. I would be annoyed if they weren't there.
adonovan 6y ago
Just to clarify: Steele has been documenting, not perpetrating, the abuse. See for example https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150_PUBLICATION_ID:5323 https://labs.oracle.com/pls/apex/f?p=94065:40150:0::::P40150...

c-cube 6y ago

If you want to reason about low level compiler optimizations, learn some assembly language. If you want to reason about type systems, learn how to read basic typing rules, it's not complicated. Sometimes planning before implementing is a good thing, or does even language design need to be agile™?

lazyjones 6y ago
What is this gibberish? I was fluent in 68k assembly 30 years ago and teaching compiler construction at university 25 years ago. Were you trying to make a point?