That program does not prove its return value under the Curry-Howard Correspondence without a lot of footwork (see first caveat). Under the CH interpretation, programs are proofs that their types are inhabited, not that they can produce their return values. Thus, the canonical thing one could say the above program proves is “int”.
Some caveats. First, one could imagine a sufficiently complex type system where there is a type of all integers which are 1. Then, one could say that the above program is a proof of the type “type-of-ints-that-are-1”. However, when adding this much specificity to one’s type system, one has to be careful that the resulting system can decidably type terms; adding richness often leads to undecidability.
Second, there is simple constructive proof that the the above program produces 1. Just run it and see; if it returns 1 in finite time, that’s a proof.
The Curry-Howard correspondence is what you are referring to right?
That program does not prove its return value under the Curry-Howard Correspondence without a lot of footwork (see first caveat). Under the CH interpretation, programs are proofs that their types are inhabited, not that they can produce their return values. Thus, the canonical thing one could say the above program proves is “int”.
Some caveats. First, one could imagine a sufficiently complex type system where there is a type of all integers which are 1. Then, one could say that the above program is a proof of the type “type-of-ints-that-are-1”. However, when adding this much specificity to one’s type system, one has to be careful that the resulting system can decidably type terms; adding richness often leads to undecidability.
Second, there is simple constructive proof that the the above program produces 1. Just run it and see; if it returns 1 in finite time, that’s a proof.
That is certainly one way to look at it.
Another way to look at it is to consider purely computational proofs, such as the four color theorem, or the solutions to checkers and 5 x 5 Go.