Curry-Howard-Lambek is a set of correspondences between logic, programming, and category theory. You may have heard of the slogan *proofs-as-programs* or *propositions-as-types*. These refer to the Curry-Howard correspondence between mathematical proofs and programs. Lambek’s name is appended to the Curry-Howard correspondence to represent connections to category theory.

The term Curry-Howard **isomorphism** is often used but is an overstatement. Logic and programming are not isomorphic, nor is either isomorphic to category theory.

You’ll also hear the term **computational trinitarianism**. That may be appropriate because logic, programming, and category theory share common attributes without being identical.

The relations between logic, programming, and categories are **more than analogies**, but **less than isomorphisms**.

There are formal correspondences between parts of each theory. And aside from these rigorous connections, there is also a heuristic that something interesting in one area is likely to have an interesting counterpart in the other areas. In that sense Curry-Howard-Lambek is similar to the **Langlands program** relating number theory and geometry, a set of theorems and conjectures as well as a sort of philosophy.

With your use of the term “computational trinitarianism” I want to make a joke about whether the correspondences are homoousiomorphisms or homoiousiamorphisms but fear the reference may be too obscure.

Well played, Jonathan.