3 ms·

I don't quite understand -- we know that, for example, correct program analysis is theoretically impossible. There is no tool to verify a general software progr

by rsj_hn 6y ago

I don't quite understand -- we know that, for example, correct program analysis is theoretically impossible. There is no tool to verify a general software program. Why should there be a tool to verify a general theorem? Verification is at least as complicated as writing the program you are verifying.

creata 6y ago
> Why should there be a tool to verify a general theorem? We want to verify proofs, not theorems. And that's far from "theoretically impossible."
- rsj_hn 6y ago
  Sorry, of course I meant to say "proof". A proof is just a more general case of a program. A program has logical operations, variables, control flow, etc. You can include all of these elements into a proof, and often do. Every program can be made into a proof, but not every proof can be made into a program. If you can verify the correctness of an arbitrary proof, you can verify the correctness of an arbitrary program. And even in practice many of the reasoning errors that happen in proofs also happen in programs -- forgetting to consider unforseen cases, not being correct about the possible ranges of variables, not anticipating all the external inputs into the program, making incorrect assertions about the state of variables, etc.
  - creata 6y ago
    > Every program can be made into a proof I'm not sure what you mean by this, but in my usage it's exactly the other way around. A proof can easily be interpreted as a program (as per the BHK and similar interpretations) but to interpret a program as a proof of something, you at least need to also formally prove that it halts. Edit: your edit clarified things a bit. The control flow in formal (and informal!) proofs is restricted compared to the control flow in programs: in order to do recursion or loops, you must have a formal argument that the recursion / loop terminates.
    - rsj_hn 6y ago
      So normally when we say "proof", we assume the proof is correct. But in this discussion we are talking about possibly incorrect proofs, with the goal of verifying the correctness of the proof. So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true. Things like loops do appear in proofs as quantifiers. So for example a proof may perform a sequence of steps in which some set is depleted, and conclude that "as we must deplete all the elements the set, the claim holds", but determining whether all elements are actually depleted by the algorithm spelled out in the proof may be hard. These types of claims appear in actual proofs, and the types of errors that are found in proofs often boil down to some case being not considered which would cause the set not to be depleted. Update: I'm unable to reply due to hn recursion limits, but as to your strictly smaller argument, that is not enough with infinite sets, which are common in proofs. Consider a proof about all surfaces, which you think you divided into a countable number of cases, but in reality there are some other types of surfaces you haven't considered. In math you are making assertions, in some sense, about the world, albeit the mathematical world, and you are claiming to have explored all the relevant parts of it for the sets of interest, but you may have not explored some parts you didn't know existed. The idea that you can formally verify such a sequence of claims is .. mind boggling. There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.
      - creata 6y ago
        This is all a bit vague, so I may be misinterpreting here. But in the given example, the proof must also prove that at each step the set is getting strictly smaller, so the computer still only has to check that the proof is correct. That is, it doesn't have to check for itself whether the set is getting smaller, it just asks you to prove that the set is getting smaller in a way that it understands. Anything more fancy than that is left up to proof automation, which is free to give up and say "nope, that leap's too big for me." > So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true. I'm not sure that's a good way of looking at it. I think the right image is to think of a proof as a program, and checking the proof as typechecking the program. The program has the additional restriction that whenever it does loops or recursion, it has to prove that something is getting strictly smaller with each iteration.
oldnews193 6y ago
> Verification is at least as complicated as writing the program you are verifying. I guess, writing a proof is basically like writing a program. Then checking a proof ought to be like *running* a program, not proving an arbitrary property of it. If your proof/program evaluates to "false", it's a wrong proof. So this is all a question of having an appropriate semantic model of computation/proof-checking, on which you can check your proof. You could then ask: "why is it that I can always run a proof? What if running it does not terminate?" To which I'd have to admit that I am really, seriously not an expert on this, but I vaguely recall that interactive theorem proving systems like Coq have a non-Turing-complete type systems. Maybe it's for a relevant reason?

by rsj_hn 6y ago

creata 6y ago

> Why should there be a tool to verify a general theorem? We want to verify proofs, not theorems. And that's far from "theoretically impossible."

rsj_hn 6y ago
Sorry, of course I meant to say "proof". A proof is just a more general case of a program. A program has logical operations, variables, control flow, etc. You can include all of these elements into a proof, and often do. Every program can be made into a proof, but not every proof can be made into a program. If you can verify the correctness of an arbitrary proof, you can verify the correctness of an arbitrary program. And even in practice many of the reasoning errors that happen in proofs also happen in programs -- forgetting to consider unforseen cases, not being correct about the possible ranges of variables, not anticipating all the external inputs into the program, making incorrect assertions about the state of variables, etc.
- creata 6y ago
  > Every program can be made into a proof I'm not sure what you mean by this, but in my usage it's exactly the other way around. A proof can easily be interpreted as a program (as per the BHK and similar interpretations) but to interpret a program as a proof of something, you at least need to also formally prove that it halts. Edit: your edit clarified things a bit. The control flow in formal (and informal!) proofs is restricted compared to the control flow in programs: in order to do recursion or loops, you must have a formal argument that the recursion / loop terminates.
  - rsj_hn 6y ago
    So normally when we say "proof", we assume the proof is correct. But in this discussion we are talking about possibly incorrect proofs, with the goal of verifying the correctness of the proof. So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true. Things like loops do appear in proofs as quantifiers. So for example a proof may perform a sequence of steps in which some set is depleted, and conclude that "as we must deplete all the elements the set, the claim holds", but determining whether all elements are actually depleted by the algorithm spelled out in the proof may be hard. These types of claims appear in actual proofs, and the types of errors that are found in proofs often boil down to some case being not considered which would cause the set not to be depleted. Update: I'm unable to reply due to hn recursion limits, but as to your strictly smaller argument, that is not enough with infinite sets, which are common in proofs. Consider a proof about all surfaces, which you think you divided into a countable number of cases, but in reality there are some other types of surfaces you haven't considered. In math you are making assertions, in some sense, about the world, albeit the mathematical world, and you are claiming to have explored all the relevant parts of it for the sets of interest, but you may have not explored some parts you didn't know existed. The idea that you can formally verify such a sequence of claims is .. mind boggling. There is a reason why very little progress has been made in formalizing math, and mistakes are sometimes discovered in even published proofs.
    - creata 6y ago
      This is all a bit vague, so I may be misinterpreting here. But in the given example, the proof must also prove that at each step the set is getting strictly smaller, so the computer still only has to check that the proof is correct. That is, it doesn't have to check for itself whether the set is getting smaller, it just asks you to prove that the set is getting smaller in a way that it understands. Anything more fancy than that is left up to proof automation, which is free to give up and say "nope, that leap's too big for me." > So let's change "proof" to set of statements/procedures which may evaluate to "true", and we need to verify that they do evaluate to true. I'm not sure that's a good way of looking at it. I think the right image is to think of a proof as a program, and checking the proof as typechecking the program. The program has the additional restriction that whenever it does loops or recursion, it has to prove that something is getting strictly smaller with each iteration.

oldnews193 6y ago

> Verification is at least as complicated as writing the program you are verifying. I guess, writing a proof is basically like writing a program. Then checking a proof ought to be like *running* a program, not proving an arbitrary property of it. If your proof/program evaluates to "false", it's a wrong proof. So this is all a question of having an appropriate semantic model of computation/proof-checking, on which you can check your proof. You could then ask: "why is it that I can always run a proof? What if running it does not terminate?" To which I'd have to admit that I am really, seriously not an expert on this, but I vaguely recall that interactive theorem proving systems like Coq have a non-Turing-complete type systems. Maybe it's for a relevant reason?