In the sense of http://en.wikipedia.org/wiki/Curry–Howard_correspondence, the theorems are the type signatures of the API, and the proofs are the implementations!