This is what is called the Curry - Howard isomorphism or even the Curry - Howard - Martin-Lof isomorphism. The formulas and types are exactly the same thing. And so, a proof of a formula is nothing but a term of a given type. So, this isomorphism is almost trivial at this level...at the level of the propositional constructive logic.

---