4 ms·
>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 isom
by 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".