Int -> Boolean is just the type of any arbitrary decidable property on Int's, so it's not very useful on its own. But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful. The proof itself need not even be constructive, since the requirement for constructibility was taken care of by providing the code for that function. Constructibility becomes more of a big deal if you want to be able to compose constructive proofs, or write proofs that rely on instances of some other proof as input, since then the strategy of providing some construction as a bare algorithm and separately proving it correct may run into problems.
And if your return type is something other than Boolean, that represents some more general construction rather than mere decidability. But everything else is just about the same. Of course this all assumes a total language with no general recursion, since otherwise you can "prove" anything by just looping forever and not delivering a result.
> But if you can endow your Int -> Boolean function with a proof that it computes some property you actually care about, that's more likely to be helpful.
Agreed, but that's beyond the scope of what's asserted with CHI, right? CHI is asserting that my implementation of some type-correct[1] (int-to-)Boolean function is, itself -- irrespective of what I can prove about it -- equivalent to some other proof. What's that proof, and what's interesting about the proof or the mapping?
[1] i.e. really does take ints and always returns bools
CHI is just the observation that some logical steps in proofs behave as similar steps in programs. For instance, "Apply Lemma f to variable x with preconditions given by H1, H2; call the resulting statement L" is equivalent to a function call L = f(x, H1, H2) where H1, H2 are capabilities or abstract "tokens". Proof by cases can be expressed as a switch { } or match { } construct, and proof by induction behaves as recursion. This often simplifies the writing of "correct by construction" programs since a single construct can take care of both the computational and the logical side.
>CHI is just the observation that some logical steps in proofs behave as similar steps in programs.
It would have to be all, not just some, or it's not an isomorphism (or there are caveats about function purity I mentioned before).
>"Apply Lemma f to variable x with preconditions given by H1, H2; call the resulting statement L" is equivalent to a function call L = f(x, H1, H2) where H1, H2 are capabilities or abstract "tokens".
Okay, that helps. So where are the mind-blowing examples?
It's not quite "all" because non-constructive proofs exist. In an ordinary program you can't just switch between returning a value as output and requesting it as an input, but in proofs you can kinda do this - and that's a logical step called "proof by contradiction".
And if your return type is something other than Boolean, that represents some more general construction rather than mere decidability. But everything else is just about the same. Of course this all assumes a total language with no general recursion, since otherwise you can "prove" anything by just looping forever and not delivering a result.