Proofs and programming

Proofs are organized a lot like programs. Based on some premises (inputs), we obtain some conclusion (output) after using a series of inference rules (basic computation like addition and other operations). Using subproofs, especially when citing previous proofs, is just like organizing our program into functions that can be used many times.

Naturally, since using inference rules is not only how people prove things, but also computers. A clear example is in type checking. The core idea of type checking a function application is “If function f takes an argument of type αα and producing an output of type ββ, and expression exp is of type αα, then f(exp) is of type ββ.” This type rule closely resembles ⇒⇒Elim: “If a proven formula is a⇒ba b and other proven formula is aa, then together, bb is a proven formula.” Furthermore, this similarity is highlighted by notation in many programming languages which would write the type of f as αα → ββ. Type rules are simply inference rules for proving results about the types of programs, and in most typical programming languages these rules closely correspond to those we are using for logic. This correspondence is known as the Curry-Howard Isomorphism.

As with logic, we want type checkers to be sound and complete. Soundness here means that if the program passes type checking, when we execute the program (or single function) and get a value, that value is of the stated type. In other words, if our program type checks, then we are guaranteed that some kinds of errors will not happen at run-time. That also means that if our program would have a run-time type error, the type checker will correctly report that our program is erroneous. Completeness here means that if we execute the program (or single function) and get a value of a certain type, then our type checker indeed tells us that type.

Note that type checking is still an area of active research, since the job is made difficult in the presence of language features such as inheritance, multiple inheritance, dynamic class loading, etc. When people introduce new computer languages with new features, and want to claim that their new language is type safe (that no function ever will be applied to the wrong type at run-time), then the paper which introduces the language will contain such a proof.