4 ms·

Yeah I'm not a fan of visual programming, but visualizing effects of programs to help with reasoning, I'm a fan of that. Proofs is my approach, but as humans we

Yeah I'm not a fan of visual programming, but visualizing effects of programs to help with reasoning, I'm a fan of that. Proofs is my approach, but as humans we don't deal with proofs as text well and have things like sequent calculus and semantic tableau that are amazing aids to reasoning.

catnaroek 9y ago
Humans can read and write proofs just fine, if they are taught how to.
- wolfgke 9y ago
  The problem is that the proofs that one finds in typical math papers are very different from the proofs for computer programs. Proofs in math papers are "mostly right" about rather complicated facts. This means that what is shown is highly non-trivial, but when an error is found, it rather does not matter since it is rather easy to fix the hole in the proof. The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for this kind of error. Proofs for computer programs rather prove statements that are rather trivial and obvious, but very subtle in the edge cases. Often the a non-formalized proof is "trivially correct" when a human skims it, but often is wrong for very, very subtle reasons. Thus there is typically no way around formalizing it - which with today's tools is very tedious and boring.
  - catnaroek 9y ago
    > The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for this kind of error. Rather than “redundancy”, it's a matter of having nice (algebraic, geometric, whatever) structure. Of course, a pure mathematician has more freedom than a programmer to decide what kinds of structures he wants to work with. > statements that are rather trivial and obvious, but very subtle in the edge cases. This is a contradiction in terms. If it seems “trivial and obvious”, but is actually “subtle in the edge cases”, then you are underestimating its complexity. > Often the a non-formalized proof is "trivially correct" when a human skims it, but often is wrong for very, very subtle reasons. Then you need to roll up your sleeves and actually prove things, not just skim through purported proofs.

catnaroek 9y ago

Humans can read and write proofs just fine, if they are taught how to.

wolfgke 9y ago
The problem is that the proofs that one finds in typical math papers are very different from the proofs for computer programs. Proofs in math papers are "mostly right" about rather complicated facts. This means that what is shown is highly non-trivial, but when an error is found, it rather does not matter since it is rather easy to fix the hole in the proof. The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for this kind of error. Proofs for computer programs rather prove statements that are rather trivial and obvious, but very subtle in the edge cases. Often the a non-formalized proof is "trivially correct" when a human skims it, but often is wrong for very, very subtle reasons. Thus there is typically no way around formalizing it - which with today's tools is very tedious and boring.
- catnaroek 9y ago
  > The reason seems to be (but this is my personal opinion) that the typical things mathematicians love to write proofs about have a high level of redundancy for this kind of error. Rather than “redundancy”, it's a matter of having nice (algebraic, geometric, whatever) structure. Of course, a pure mathematician has more freedom than a programmer to decide what kinds of structures he wants to work with. > statements that are rather trivial and obvious, but very subtle in the edge cases. This is a contradiction in terms. If it seems “trivial and obvious”, but is actually “subtle in the edge cases”, then you are underestimating its complexity. > Often the a non-formalized proof is "trivially correct" when a human skims it, but often is wrong for very, very subtle reasons. Then you need to roll up your sleeves and actually prove things, not just skim through purported proofs.