A proof is a program. Proofs are broken down into terms Functions in a program can be broken down into Quantifier and Predicate A formula is a type.