5 ms·

The Curry-Howard correspondence would like a word. Any time you write a program, you are also writing a proof. Mechanized proof checkers leverage this idea to

The Curry-Howard correspondence would like a word. Any time you write a program, you are also writing a proof. Mechanized proof checkers leverage this idea to enable users to specify formal proofs as programs.

Jensson 5y ago
Programs are proofs in the same way solutions to arithmetic's problems are proofs, they typically don't prove anything interesting so are not considered proofs even though in practice you could map every program to some set of mathematical statements and vice versa. Edit: And for this topic in question, If you don't understand what you are proving then you aren't working with proofs. I really doubt that programmers actually constructs their programs by mapping it to mathematical statements, seeing what it proves and then mapping it back to a program, so they are writing programs, not proofs.
gjm11 5y ago
The Curry-Howard isomorphism doesn't say that an interesting proof corresponds to a program anyone would care about (other than as an equivalent to the proof), nor that an interesting program corresponds to a proof anyone would care about (other than as an equivalent to the program). In practice, writing programs and finding proofs feel like quite different activities, and at least in my experience of doing both I almost never try to write a program by thinking "how could I prove that such-and-such a type is nonempty" and I literally never try to prove something by finding a corresponding type and writing a program that computes or represents something of that type. The Curry-Howard isomorphism is a beautiful theorem, and as you say it inspires some nice methods of automated proving / proof-checking, but I don't think it says anything much about the relationship between the programming and theorem-proving activities that actual humans engage in.
AnimalMuppet 5y ago
> Any time you write a program, you are also writing a proof. True, and (mostly) irrelevant. When I write a program, I am also writing a proof, but I don't care about it as a proof. It proves something that I am completely uninterested in proving. But as a program, it's a program that I am interested in running.
- warrenm 5y ago
  > It proves something that I am completely uninterested in proving. But as a program, it's a program that I am interested in running. Interesting that you contradict yourself in successive sentences By running the program, you, in fact, demonstrate that you are quite interested in proving whatever it is you wrote
  - drdeca 5y ago
    You don’t care what the statement it proves is, and just an assurance of the conclusion would often be not valued
  - AnimalMuppet 5y ago
    > Interesting that you contradict yourself in successive sentences No, I didn't. You managed to either completely miss my point, or to completely ignore it. Just in case you didn't ignore it, let me try again. I could care about a proof for the sake of the proof. If that were the case, I probably wouldn't write a program, I'd just write the proof. (Yes, that could be mechanically turned into a program, but I didn't actually do that, because I cared about the proof rather than the program.) When I write a program, I usually care about it as a program, not as a proof. When I write a GUI, say, I care about how it enables the users to access the rest of the program's features. You can turn that into a proof, and the compiler may in fact do so, but what it proves is something that is really unrelated to what I'm trying to do. The "proof" won't prove anything about usability or human factors or pleasing color scheme or user workflow or efficient use of screen real estate. It will prove something that, from the programming point of view, is completely uninteresting. So, as I said, I'm not interested in the proof, I'm interested in the program. And, despite the correspondence, they are not the same thing.
    - warrenm 5y ago
      >I'm not interested in the proof, I'm interested in the program Maybe not in the abstract - but you are, in fact, "interested in the proof": because when the program doesn't do what you want it to, you either have to fix it so it does prove your use case, or you've proven that what you were trying to do was incorrect

Jensson 5y ago

Programs are proofs in the same way solutions to arithmetic's problems are proofs, they typically don't prove anything interesting so are not considered proofs even though in practice you could map every program to some set of mathematical statements and vice versa. Edit: And for this topic in question, If you don't understand what you are proving then you aren't working with proofs. I really doubt that programmers actually constructs their programs by mapping it to mathematical statements, seeing what it proves and then mapping it back to a program, so they are writing programs, not proofs.

gjm11 5y ago

The Curry-Howard isomorphism doesn't say that an interesting proof corresponds to a program anyone would care about (other than as an equivalent to the proof), nor that an interesting program corresponds to a proof anyone would care about (other than as an equivalent to the program). In practice, writing programs and finding proofs feel like quite different activities, and at least in my experience of doing both I almost never try to write a program by thinking "how could I prove that such-and-such a type is nonempty" and I literally never try to prove something by finding a corresponding type and writing a program that computes or represents something of that type. The Curry-Howard isomorphism is a beautiful theorem, and as you say it inspires some nice methods of automated proving / proof-checking, but I don't think it says anything much about the relationship between the programming and theorem-proving activities that actual humans engage in.

AnimalMuppet 5y ago

> Any time you write a program, you are also writing a proof. True, and (mostly) irrelevant. When I write a program, I am also writing a proof, but I don't care about it as a proof. It proves something that I am completely uninterested in proving. But as a program, it's a program that I am interested in running.

warrenm 5y ago
> It proves something that I am completely uninterested in proving. But as a program, it's a program that I am interested in running. Interesting that you contradict yourself in successive sentences By running the program, you, in fact, demonstrate that you are quite interested in proving whatever it is you wrote
- drdeca 5y ago
  You don’t care what the statement it proves is, and just an assurance of the conclusion would often be not valued
- AnimalMuppet 5y ago
  > Interesting that you contradict yourself in successive sentences No, I didn't. You managed to either completely miss my point, or to completely ignore it. Just in case you didn't ignore it, let me try again. I could care about a proof for the sake of the proof. If that were the case, I probably wouldn't write a program, I'd just write the proof. (Yes, that could be mechanically turned into a program, but I didn't actually do that, because I cared about the proof rather than the program.) When I write a program, I usually care about it as a program, not as a proof. When I write a GUI, say, I care about how it enables the users to access the rest of the program's features. You can turn that into a proof, and the compiler may in fact do so, but what it proves is something that is really unrelated to what I'm trying to do. The "proof" won't prove anything about usability or human factors or pleasing color scheme or user workflow or efficient use of screen real estate. It will prove something that, from the programming point of view, is completely uninteresting. So, as I said, I'm not interested in the proof, I'm interested in the program. And, despite the correspondence, they are not the same thing.
  - warrenm 5y ago
    >I'm not interested in the proof, I'm interested in the program Maybe not in the abstract - but you are, in fact, "interested in the proof": because when the program doesn't do what you want it to, you either have to fix it so it does prove your use case, or you've proven that what you were trying to do was incorrect