4 ms·

The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. Just because a computer beeps and says "pro

by Retra 8y ago

The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. Just because a computer beeps and says "proof correct" doesn't mean you've proven what you thought you have, so we need to first translate the logic in which your assumptions are derived into the logic of the machine. That is a complex and subtle project. In other words, it's actually very easy to prove something with a computer, but it's very difficult to prove the thing you actually set out to prove. It's not any easier than writing a bug-free program.

singularity2001 8y ago
Would it be possible to simplify the system by making default assumptions about a consensus/common-sense logic? Are topologists interested in different logical foundations?
- alimw 8y ago
  You're right (and the GP isn't). A proof of your topological theorem in any one of Coq/Isabelle/Lean is a pretty good indication that it's correct, in spite of their various foundations.
  - Retra 8y ago
    ... assuming you correctly wrote your theorem in those frameworks.
    - alimw 8y ago
      I think you are exaggerating the difficulty of theorem statement compared to proof. Here is one (admittedly extreme) example in Lean, from the formal abstracts website. theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare
Jweb_Guru 8y ago
Oh, come on. "It's not any easier than writing a bug-free program" is not even remotely true. Getting the spec right is way easier than getting the implementation right, in almost all cases. And the logic isn't that different from set theory--there's even a set theoretic model (which you get when you use Prop, to which you can add classical axioms).
- mannykannot 8y ago
  If getting the spec right is way easier than getting the implementation right, then strict waterfall would be the most effective way to write programs, and the holy grail of software engineering would be to automate the process of generating implementations from formal specs (there are some people who think exactly that, but that has been the case for about five decades, with effectively no impact on how software is actually made.) The reality is that we often overlook issues with the spec until we try to implement it, or try using what we have implemented, even when we are trying to get the spec right first.
  - Jweb_Guru 8y ago
    I have no idea where you're going with this, but getting the spec right is very different from actually finding a proof for it. I never said actually finding the proof was always easy. But I will say this for sure: getting the spec right and finding a proof for it are jointly much easier than writing a nontrivial bug-free program without a theorem prover. The success or lack of success of waterfall is not relevant here, as that has very little to do with formal verification; additionally, the success of most software methodologies is not measured solely on whether the end product was correct.
- Retra 8y ago
  If programmers sat around writing <10K line pure programs with no user interaction, they would have just as lovely a time as Mathematicians. If theorem proving in mathematics is easy for you, it is because your aren't trying to prove hard things.
  - 8y ago
chriswarbo 8y ago
> The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. If you're referring to the fact that many proof assistants (e.g. Coq) are based on constructive/intuitionistic type theory, whilst most mathematics is formulated in classical set theory, then yes there is some translation involved. However, I would point out that we can use classical logic pretty easily by adding excluded middle, double negation elimination, etc. to an intuitionistic system (this is available in the Coq standard library https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html ). There are also systems which can use set theory (directly or indirectly), like Metamath and Isabelle. Personally, I much prefer type theory (which I self-learned, before pursuing a related PhD) to set theory (which I was taught as an undergraduate and enjoyed, but not enough to do it as a hobby). However, I'm well aware that my computer scientist background is nothing like that of a trained mathematician.

by Retra 8y ago

singularity2001 8y ago

Would it be possible to simplify the system by making default assumptions about a consensus/common-sense logic? Are topologists interested in different logical foundations?

alimw 8y ago
You're right (and the GP isn't). A proof of your topological theorem in any one of Coq/Isabelle/Lean is a pretty good indication that it's correct, in spite of their various foundations.
- Retra 8y ago
  ... assuming you correctly wrote your theorem in those frameworks.
  - alimw 8y ago
    I think you are exaggerating the difficulty of theorem statement compared to proof. Here is one (admittedly extreme) example in Lean, from the formal abstracts website. theorem Wiles_Taylor : ∀ (x y z n : nat), x > 0 → y > 0 → n > 2 → x ^ n + y ^ n ≠ z ^ n := more years than I have to spare

Jweb_Guru 8y ago

Oh, come on. "It's not any easier than writing a bug-free program" is not even remotely true. Getting the spec right is way easier than getting the implementation right, in almost all cases. And the logic isn't that different from set theory--there's even a set theoretic model (which you get when you use Prop, to which you can add classical axioms).

mannykannot 8y ago
If getting the spec right is way easier than getting the implementation right, then strict waterfall would be the most effective way to write programs, and the holy grail of software engineering would be to automate the process of generating implementations from formal specs (there are some people who think exactly that, but that has been the case for about five decades, with effectively no impact on how software is actually made.) The reality is that we often overlook issues with the spec until we try to implement it, or try using what we have implemented, even when we are trying to get the spec right first.
- Jweb_Guru 8y ago
  I have no idea where you're going with this, but getting the spec right is very different from actually finding a proof for it. I never said actually finding the proof was always easy. But I will say this for sure: getting the spec right and finding a proof for it are jointly much easier than writing a nontrivial bug-free program without a theorem prover. The success or lack of success of waterfall is not relevant here, as that has very little to do with formal verification; additionally, the success of most software methodologies is not measured solely on whether the end product was correct.
Retra 8y ago
If programmers sat around writing <10K line pure programs with no user interaction, they would have just as lovely a time as Mathematicians. If theorem proving in mathematics is easy for you, it is because your aren't trying to prove hard things.
- 8y ago

chriswarbo 8y ago

> The painful part is that you're using tools which are trying to bridge between wildly different logical foundations. If you're referring to the fact that many proof assistants (e.g. Coq) are based on constructive/intuitionistic type theory, whilst most mathematics is formulated in classical set theory, then yes there is some translation involved. However, I would point out that we can use classical logic pretty easily by adding excluded middle, double negation elimination, etc. to an intuitionistic system (this is available in the Coq standard library https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html https://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html ). There are also systems which can use set theory (directly or indirectly), like Metamath and Isabelle. Personally, I much prefer type theory (which I self-learned, before pursuing a related PhD) to set theory (which I was taught as an undergraduate and enjoyed, but not enough to do it as a hobby). However, I'm well aware that my computer scientist background is nothing like that of a trained mathematician.