3 ms·

> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every map

by dvt 10y ago

> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof! For those of you that may not know, this is called the Curry-Howard(-Lambek) Correspondence[1]. It establishes an isomorphism between well-formed computer programs and formal logic. This isomorphism is fairly intuitive when doing something like (typed) λ-calculus, but it also applies to things like Java and C++. [1] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Chinjut 10y ago
Yes, Bob Harper is aware of, and intentionally discussing precisely, this. (The "Curry-Howard-Lambek" correspondence, if you like)
- dvt 10y ago
  He's a PhD in CS so I assumed he did :) I linked it for other people that may not know that it's a thing. The article itself is a bit hand-wavy.
  - aminorex 10y ago
    Extremely so. Lacking so much as useful keywords for finding what he refers to as "standard sources".
mafribe 10y ago
Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means inconsistency if you interpret types as truth-bearing propositions. Currently Curry-Howard mostly only works for strongly normalising, pure functional languages. It's also not clear if Curry-Howard is really an isomorphism. For a map to be an isomorphism, structure has to be preserved in both directions, but what is the structure on proofs? That's a wide open question. We can't even agree on what it means for proofs to be equal. (The structure of is the content of Hilbert's 24th problem that he decided not to include in his famous 23 problems [1].) It's better to speak of the Curry-Howard correspondence. [1] https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob...
- chriswarbo 10y ago
  > Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means inconsistency if you interpret types as truth-bearing propositions. Currently Curry-Howard mostly only works for strongly normalising, pure functional languages. As far as I'm aware, a complicated, inscrutable, unsound logic is still a logic. It's debatable whether it's a useful logic, but even that's not a fatal flaw for these languages, seeing as their main design focus is making normalisation of programs/proofs convenient. I suppose the two perspectives of Curry-Howard aren't so much about proving/programming as they are about caring-about-the-theorem/caring-about-the-proof. The existence of non-termination is a problem if you care about theorems, since you can't trust proofs and must deal with them manually to see if they're doing anything fishy. Java and C++ care so much about proofs that they don't really understand what else you might want to do other than dealing with proofs (programs) manually. If you presented a C++ programmer with an automated theorem prover (given a C++ type signature, return a C++ program fragment of that type) I imagine they wouldn't be particularly impressed, since types are just one small part of the concerns that a C++ programmer has.
  - mafribe 10y ago
    unsound logic is still a logic Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.
    - chriswarbo 10y ago
      I would hedge my bets, and say that soundness is often a useful property of logics, especially when they're used for proving theorems/conjectures. In the case of C++ and Java, they're not often (ever?) used for proving, yet Curry-Howard tells us that they are logics. Curry-Howard goes both ways, it's not a reduction of programming to theorem proving; if it were, then we could write optimising compilers for all dynamically typed languages, which output "null" for every input. Likewise, mathematics cannot be summarised as "getting stuff to compile". Instead, the concerns and interests of the practitioners from both sides are unchanged by Curry-Howard; it just tells us that both those groups are actually working within the same context, and hence they may be able to share ideas/tools/techniques/etc. Whilst an unsound logic might be useless to a logician, a programmer (or even computer scientist!) may not care too much, since they might be much more concerned about, say, the computational complexity of an algorithm rather than its types.

by dvt 10y ago

Chinjut 10y ago

Yes, Bob Harper is aware of, and intentionally discussing precisely, this. (The "Curry-Howard-Lambek" correspondence, if you like)

dvt 10y ago
He's a PhD in CS so I assumed he did :) I linked it for other people that may not know that it's a thing. The article itself is a bit hand-wavy.
- aminorex 10y ago
  Extremely so. Lacking so much as useful keywords for finding what he refers to as "standard sources".

mafribe 10y ago

Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means inconsistency if you interpret types as truth-bearing propositions. Currently Curry-Howard mostly only works for strongly normalising, pure functional languages. It's also not clear if Curry-Howard is really an isomorphism. For a map to be an isomorphism, structure has to be preserved in both directions, but what is the structure on proofs? That's a wide open question. We can't even agree on what it means for proofs to be equal. (The structure of is the content of Hilbert's 24th problem that he decided not to include in his famous 23 problems [1].) It's better to speak of the Curry-Howard correspondence. [1] https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_problem https://en.wikipedia.org/wiki/Hilbert%27s_twenty-fourth_prob...

chriswarbo 10y ago
> Curry-Howard is not known to apply to Java and C++. That's because the typing systems of these languages are no logics. For a start, in both languages, you can write non-terminating programs, hence any type is inhabited, which means inconsistency if you interpret types as truth-bearing propositions. Currently Curry-Howard mostly only works for strongly normalising, pure functional languages. As far as I'm aware, a complicated, inscrutable, unsound logic is still a logic. It's debatable whether it's a useful logic, but even that's not a fatal flaw for these languages, seeing as their main design focus is making normalisation of programs/proofs convenient. I suppose the two perspectives of Curry-Howard aren't so much about proving/programming as they are about caring-about-the-theorem/caring-about-the-proof. The existence of non-termination is a problem if you care about theorems, since you can't trust proofs and must deal with them manually to see if they're doing anything fishy. Java and C++ care so much about proofs that they don't really understand what else you might want to do other than dealing with proofs (programs) manually. If you presented a C++ programmer with an automated theorem prover (given a C++ type signature, return a C++ program fragment of that type) I imagine they wouldn't be particularly impressed, since types are just one small part of the concerns that a C++ programmer has.
- mafribe 10y ago
  unsound logic is still a logic Hmmm ... If your logic is unsound, anything can be proven. Soundness is a key requirement of any logic for this reason.
  - chriswarbo 10y ago
    I would hedge my bets, and say that soundness is often a useful property of logics, especially when they're used for proving theorems/conjectures. In the case of C++ and Java, they're not often (ever?) used for proving, yet Curry-Howard tells us that they are logics. Curry-Howard goes both ways, it's not a reduction of programming to theorem proving; if it were, then we could write optimising compilers for all dynamically typed languages, which output "null" for every input. Likewise, mathematics cannot be summarised as "getting stuff to compile". Instead, the concerns and interests of the practitioners from both sides are unchanged by Curry-Howard; it just tells us that both those groups are actually working within the same context, and hence they may be able to share ideas/tools/techniques/etc. Whilst an unsound logic might be useless to a logician, a programmer (or even computer scientist!) may not care too much, since they might be much more concerned about, say, the computational complexity of an algorithm rather than its types.