4 ms·

My comment was not to imply that software will replace people “doing math”, but that the math which is “done” will be encoded in a standard format that can be r

My comment was not to imply that software will replace people “doing math”, but that the math which is “done” will be encoded in a standard format that can be reused (and verified) more readily. Really, this is about software—if you want to do anything with a computer, it must be formalized. Some of this formalization takes place before a line of code is written, usually in the form of mathematical statements. I’d argue that this part of the process ought to be standardized just like library code is standardized, or we will be carrying a very heavy load of collective technical debt as software is asked to do more and more complex and high-assurance tasks.

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

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