3 ms·
> 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. Agre
by SilasX 3y ago
> 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
- zozbot234 3y agoCHI 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.
- SilasX 3y ago>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?
- kaba0 3y agoI am absolutely not an expert here, but you probably want dependent types to have more interesting examples. Hopefully my made up syntax is understandable fermat x y z: Int -> Int -> Int -> c: (x^z+y^z=c^z and Int) This might only ever have an implementation if we hard code it to z=2.
- zozbot234 3y agoIt'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".
- deleted 3y ago[deleted]