>Every type system is a system of logic (and vice-versa.) * So, if you have a System F, you can build a Haskell. * If you have affine logic, you can make Rust.
That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages; if the latter is more general it probably should have, and would have, been phrased that way.
>Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time.
Sorry, what's the connection to CHI here?
>It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4.
I meant "non-trivial" to apply to the mapping as well. As best I can tell, CHI just says there's some useless program that maps to every proof, and a useless proof that maps to every program. So what? What is the significance of that? So I can write a meaningless program that corresponds to Pons Asinorum?
You're not really taking the challenge seriously here -- you're just asserting the same trivialities about which I was asking, "is that all there is?"
> That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages
But proofs are written in systems of logic and programs are written in (programming) languages, so if there's a correspondence between the first there really ought to be a correspondence between the second!
That seems to be different from CHI, which asserts a correspondence between proofs and programs, not between systems of logic and languages; if the latter is more general it probably should have, and would have, been phrased that way.
>Have a look at this parser combinator library[1]. In particular look at how many functions are marked "Totality: total". These are functions which accept all (well-typed) inputs and terminate in finite time.
Sorry, what's the connection to CHI here?
>It would just be a program - that you write every day. If Pons Asinorum is expressed in twenty lines, then pick a twenty-line program. If you want something bigger, check out CakeML or seL4.
I meant "non-trivial" to apply to the mapping as well. As best I can tell, CHI just says there's some useless program that maps to every proof, and a useless proof that maps to every program. So what? What is the significance of that? So I can write a meaningless program that corresponds to Pons Asinorum?
You're not really taking the challenge seriously here -- you're just asserting the same trivialities about which I was asking, "is that all there is?"