5 ms·

> 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 ca

> 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.
  - mafribe 10y ago
    Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.
    - dvt 10y ago
      Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic insofar that it follows the same rules as the proposition A → B where A is true: A → B A ∴ B (I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.) [1] http://dvt.name/logic/horse2.pdf http://dvt.name/logic/horse2.pdf
      - mafribe 10y ago
        It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.
        dvt 10y ago
        There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much. All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have. [1] http://plato.stanford.edu/entries/logic-paraconsistent/ http://plato.stanford.edu/entries/logic-paraconsistent/
        mafribe 10y ago
        C++ and Java are not even paraconsistent: every type is inhabited.
      - 10y ago
- dvt 10y ago
  This is actually wrong.. There's an old joke in logic: sound, complete, consistent -- pick two :) I think you're misunderstanding what soundness is. Soundness means that a proof in that logic implies a (semantic) entailment in that logic. That is: Γ ⊢ A ⇒ Γ ⊨ A It's a very specific characteristic.
  - mafribe 10y ago
    Sorry, I mean inconsistent where I wrote sound.
    - jsprogrammer 10y ago
      I'm still not sure it's true that an inconsistent logic can prove anything. Certainly an inconsistent logic contains contradictory proofs, but I don't think every inconsistent logic can be used to "prove" any arbitrary theorem.

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.
- mafribe 10y ago
  Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.
  - dvt 10y ago
    Any typing system that has at least two types (functional and non-functional) is a logic. In fact, modus ponens follows axiomatically via →elimination: Let α → H be a functional type where α is a Person type, and H is a boolean type. Γ ⊢ α → H Γ ⊢ α --------------------- (→e) Γ ⊢ H What this means is that you can have a function isAtHome(x) which takes a Person and returns a boolean. This schema itself is a logic insofar that it follows the same rules as the proposition A → B where A is true: A → B A ∴ B (I wrote a simple and short paper[1] about typing λ-calculus in the context of Frege's concept horse paradox a few years ago.) [1] http://dvt.name/logic/horse2.pdf http://dvt.name/logic/horse2.pdf
    - mafribe 10y ago
      It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.
      - dvt 10y ago
        There are many paraconsistent logics out there[1]. There are also many "trivial" logics out there[1] (which exhibit the Principle of Explosion). The former are useful, the latter not so much. All them of them are logics. Consistency is not a requirement; it's simply a property a system may or may not have. [1] http://plato.stanford.edu/entries/logic-paraconsistent/ http://plato.stanford.edu/entries/logic-paraconsistent/
        mafribe 10y ago
        C++ and Java are not even paraconsistent: every type is inhabited.
    - 10y ago
dvt 10y ago
This is actually wrong.. There's an old joke in logic: sound, complete, consistent -- pick two :) I think you're misunderstanding what soundness is. Soundness means that a proof in that logic implies a (semantic) entailment in that logic. That is: Γ ⊢ A ⇒ Γ ⊨ A It's a very specific characteristic.
- mafribe 10y ago
  Sorry, I mean inconsistent where I wrote sound.
  - jsprogrammer 10y ago
    I'm still not sure it's true that an inconsistent logic can prove anything. Certainly an inconsistent logic contains contradictory proofs, but I don't think every inconsistent logic can be used to "prove" any arbitrary theorem.