[dvt]

> 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_correspon...

[mafribe]

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_prob...

[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

[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.

[Chinjut]

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

[dvt]

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]

Extremely so. Lacking so much as useful keywords for finding what he refers to as "standard sources".