ughly the same kind of generic
computational power as lambda calculus, but was actually discovered before it.

The abstract formal equivalence between these two systems
is officially called the "Curry-Howard Isomorphism" (CHI),
but more often, the "propositions as types" (PAT) analogy.

For example, PAT gives a correspondence
between the propositional equivalence

[A &amp; B =&gt; C]  &lt;=&gt;  [A =&gt; [B =&gt; C]]

and the functional-type isomorphism

[A x B -&gt; C]  ~=~  [A -&gt; [B -&gt; C]].

In the 