Curry-Howard, logically

I tend to think of the Curry-Howard correspondence from the point of view of types: I repeat the slogan "types are propositions about programs" in my head, and that helps me remember that the types correspond to logical propositions, and the programs correspond to proofs of those propositions.

But upon reading the introduction to Proofs and Types, I was reminded of the parallel point of view of proofs. If we think of proofs as mathematical objects, then we can give them natural representations: a proof of A ∧ B is representable as a pair of proofs of A and B, respectively; a proof of A ∨ B is represented as a discriminated union of either a proof of A or a proof of B; and most importantly, a proof of A ⇒ B is representable as a function that takes any proof of A and produces a proof of B.