[chriswarbo]

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

   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]

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]

Can you explain to me in what sense the Java and C++ typing systems are logics? Because I don't see it.

[dvt]

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

[chriswarbo]

Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

I was struggling to think of a concrete example less trivial than function application, but I suppose my difficulty just shows how terrible these systems are when viewed as logics (but they're still logics!)

[dvt]

> Thanks, this is what I was getting at: the type systems of C++ and Java are logics in the sense of being formal syntactic systems with deduction rules.

Yep, exactly. Why I think it's hard to think of a more concrete example is because any type theory (like vanilla λ-calculus) is not deductive.

Let me clarify: once you add types to λ-calculus, it (amazingly) becomes deductive! But the type theory itself is not deductive (because types are not tractable, among other reasons).

[mafribe]

It's not enough for a formalism to exhibit modus ponens to be a logic. It also needs to be consistent.

[dvt]

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/

[dvt]

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]

Sorry, I mean inconsistent where I wrote sound.