Final remark

• Types are propositions

• Programs are their proofs

• In languages like Agda, types are explicitly propositions

• The 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