Types and Correctness

While in practice full correctness proofs are rarely forthcoming, computer scientists still employ tools that guarantee some form of correctness. One of these tools is a type checker for the language. Types fine-tune the grammatical structure of the language, and bring semantic intuitions to the grammatical party. The following is a quote from Pierce’s text on types in programming languages.