# Curry-Howard is overrated

(*original title*: "Curry Howard is a scam". See below.)

The
Curry-Howard correspondence
has been talked about a lot recently, not only in Haskell circles, but also
among CiC-based proof assistant practitioners (Coq, Lean, etc.).
In a nutshell, it makes a deep parallel between "programs" (terms of some flavor
of lambda calculus, typically), and "proofs" (these programs are a proof of their type,
or more precisely they are witnesses that their types are inhabited).
The most basic example is `id x = x`

which, in Haskell, would be a proof of
$ \forall a. a \rightarrow a $, a trivial theorem of propositional logic.

That's all good and well, but my point here is that *in practice*, the equivalence is
not as interesting as it first looks.