Next | Types Are Theorems; Programs Are Proofs | 32 |

Types are propositions

Programs are their proofs

In languages like Agda, types are

*explicitly*propositionsThe type of a sorting function might include an assertion that the results are correctly sorted

a -> b :: List a ∧ List b ∧ length(a) = length(b) ∧ sortedOrder(b) ∧ subset(a, b) ∧ subset(b, a)

The sorting function itself would be a proof of this assertion

The Agda typechecker would derive the proof of the correctness of the sorter

If it failed to do so, you would know your program had a bug

The failure of the proof would tell you where

Next | Next |