4 ms·

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 looki

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

by jlouis 6y ago

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