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.