I came upon the Curry-Howard Isomorphism relatively late in my programming life, and perhaps this contributes to my being utterly fascinated by it. It implies that for every programming concept there exists a precise analogue in formal logic, and vice versa. Here's a "basic" list of such analogies, off the top of my head:

```
program/definition | proof
type/declaration | proposition
inhabited type | theorem/lemma
function | implication
function argument | hypothesis/antecedent
function result | conclusion/consequent
function application | modus ponens
recursion | induction
identity function | tautology
non-terminating function | absurdity/contradiction
tuple | conjunction (and)
disjoint union | disjunction (or) -- corrected by Antal S-Z
parametric polymorphism | universal quantification
```

So, to my question: **what are some of the more interesting/obscure implications of this isomorphism?** I'm no logician so I'm sure I've only scratched the surface with this list.

For example, here are some programming notions for which I'm unaware of pithy names in logic:

```
currying | "((a & b) => c) iff (a => (b => c))"
scope | "known theory + hypotheses"
```

And here are some logical concepts which I haven't quite pinned down in programming terms:

```
primitive type? | axiom
set of valid programs? | theory
```

Edit:

Here are some more equivalences collected from the responses:

```
function composition | syllogism -- from Apocalisp
continuation-passing | double negation -- from camccann
```

`goto | jumping to conclusions`

model1more comment