Chapter 4: Polymorphism

Chapter 3 ended one step short. Everything it proved was proved from no hypotheses at all, and nothing worth proving about a program is like that. Here are two things you would actually want to know.

The first is a bug report: “discount not applied on the last day of the sale.” A model proposes the fix below, a reviewer approves it, and the tests pass.

- return start <= today && today <= end; 
+ return start <  today && today <  end;

Is the patch correct? It makes the failing test pass. It also silently removes the discount on the first day of the sale, and no test covers that. It is perfectly well typed: no compiler will ever object to it, and by everything in Chapters 1–3 it is safe to run. Every yes you could give it rests on something nobody has checked — and what nobody has checked is what a sale is: that the discount applies on every day from the start to the end, those two included.

The second is what a sorting routine promises: that in the list it hands back, every element is at most the next one. Neither claim is a formula of Chapter 3. Both say for all, and that chapter had no way to say it; worse, it had no way even to name the things being quantified over — the days, the positions in a list — since its letters $p$, $q$, $r$ stood for whole claims and had nothing inside them.

So two things are missing, and the first is a language: one with terms that name things, predicates that say something about them, and quantifiers that range over them. That language is the subject of §4.1, and it is the language the rest of this course is written in.

The second missing thing is the rules, and here you are further ahead than you think. You have been writing $\forall$ for years without noticing. The type of length is [a] -> Int, which with the quantifier it silently carries is

and your compiler has rules for that $\forall$ which it applies hundreds of times a second. They range over types rather than over days or list positions, so they are not the same quantifier — but they are the same rules, side conditions included, and §4.2 sets out the type theory they belong to before §4.3 writes them as logic. The chapter then ends where this part has been going: a sorting contract, proved.

4.1 First-order syntax

A type says what kind of thing a value is: this is an integer, that is a list of strings. It cannot say anything about which integer, and a specification is about which. To write “the discount applies on every day of the sale” we need symbols for days, for the start and the end, for the relation is on or after, and a way to say every. Here is the language that supplies them, and it is the one Frege arrived at in 1879 and nobody has had to replace.

A term names a thing; a formula makes a claim. Keep the two apart, as a parser would by giving them different types. In $x+1<y$ the symbols $1$ and $+$ are a constant and a function symbol, $<$ is a predicate symbol, and $x$ and $y$ are variables; $x+1$ is a term and $x+1<y$ a formula, and it would be a type error to write either where the other belongs. Here is the signature this chapter uses for its second half, which is an access-control policy — the rules that decide who may read what. The constants are users and resources, $\mathrm{𝑎𝑙𝑖𝑐𝑒}$ and $\mathrm{𝑐𝑜𝑛𝑓𝑖𝑔}$; the predicates are

A policy is then a set of formulas. “Administrators may read everything” is $\forall x\forall y(\mathrm{𝐴𝑑𝑚𝑖𝑛}(x)\to \mathrm{𝐶𝑎𝑛𝑅𝑒𝑎𝑑}(x,y))$; “owners may read what they own” is $\forall x\forall y(\mathrm{𝑂𝑤𝑛𝑠}(x,y)\to \mathrm{𝐶𝑎𝑛𝑅𝑒𝑎𝑑}(x,y))$. Those are sentences a security team writes in English and a system enforces in code, and the question “can Alice read the config file?” is the question whether a particular formula follows from them. By the end of this chapter that question has a certificate.

In $\forall x(x<y)\to \exists y(x=y)$ the first two occurrences of $x$ are bound and the third free; the first $y$ is free and the second bound; so this is a formula but not a sentence. The term $y$ is not substitutable for $x$ in $\exists y(x=y)$, since it would be captured; the term $z$ is. §4.3 shows what goes wrong when the condition is dropped, and that it is a bug you have already met.

4.2 Polymorphic type theory

Now the type system, built the way Chapters 1 and 3 built theirs: types, terms, judgements, rules, and then some typings written out. What is added to Chapter 3 is a quantifier over types, and two rules for it. First, why anyone wants one. Ask what type length should have. It takes a list and returns a number, but a list of what? Of anything. Without a way to say of anything you have three options, and all are bad.

• Write lengthOfIntList, lengthOfStringList, and one more for every element type you ever use. That is the same code copied until one copy is fixed and the others are not.
• Give length the type [Object] -> Int and cast on the way in and out. This is what Java made people do until 2004, and the casts are unchecked: what used to be a compile error has become an exception in production.
• Turn the checker off for that part of the program. This is where dynamic languages start and where the Mars Climate Orbiter ended.

One piece of code, one proof of safety, every element type at once, and nothing unchecked anywhere: that is what the quantifier buys, and it is why map, filter, sort, every container and every interface worth the name have it in their types.

A type variable in the context is a type nobody has chosen yet. That is the only new idea here, and the two rules both turn on it.

Read ($\forall$E) first, because it is the one you use every time you call a library function: a program that works for every $a$ may be used at any particular $B$, and using it is substituting $B$ for $a$ throughout its type. Read ($\forall$I) as what happens when a definition is finished: if you typed the body with $a$ in the context — that is, with $a$ standing for no type in particular — then the program works for every $a$, and you may say so. Proved for an arbitrary $a$, hence for all.

The side condition, which you have met as an error message. Rule ($\forall$I) carries a proviso, and it is the only interesting one in this chapter. Generalising over $a$ is allowed only when $a$ is genuinely arbitrary, which means: fixed by no typing still in the context. Line 3 of Example 4.4 was legal because the context was empty by then. Inside the body it would not have been. With $x:a$ still in the context we may not conclude $x:\forall aa$, because that would make $x$ a value of every type at once, and $x$ is one particular value whose type the caller will choose. Try it:

f :: a -> b 
f x = x

and GHC answers couldn’t match expected type b with actual type a, adding that a is a rigid type variable bound by the signature. The signature promised a program that works for every $a$ and every $b$ separately; the body only works when they are the same. The compiler is enforcing the proviso on ($\forall$I), and §4.3 will write the same proviso as a side condition on a rule of logic, where it does the same job and catches the same mistake.

The other quantifier, and the code it is made of. A type can also hide something. Suppose you want a counter: a thing with a starting state, a way to step it, and a way to read off a number. You do not want to say what the state is, because that is the implementation’s business. In Haskell:

{-# LANGUAGE ExistentialQuantification #-} 
data Counter = forall a. MkCounter a (a -> a) (a -> Int) 
intCounter  = MkCounter (0 :: Int)   (+1)    id 
listCounter = MkCounter ([] :: [()]) (():)   length 
tick3 :: Counter -> Int 
tick3 (MkCounter s step out) = out (step (step (step s)))

Both intCounter and listCounter are values of the one type Counter, although one carries an Int and the other a list, and tick3 returns 3 for each without being told which. The type of Counter is

there is a type with these three operations. Its two rules are building and taking apart, and they are what MkCounter and the pattern match in tick3 do:

($\exists$I) is the constructor: supply the hidden type $B$ and a value of the interface at that type, and out comes a value that mentions neither. ($\exists$E) is the pattern match: you may use the package to produce anything you could have produced from a fresh type variable $a$ and a value of the interface at $a$.

The side condition on ($\exists$E) is the abstraction barrier, and it is worth seeing what it forbids. tick3 returns an Int, which does not mention $a$, so it type-checks. A function that tried to return the counter’s state would have result type $a$, and $a$ is free in that result type, so ($\exists$E) refuses. Try it and GHC says the rigid type variable a would escape its scope — the same words, almost, as before, enforcing the same kind of condition. The implementation type may be used inside the match and may not leave it. That is what makes a module boundary a boundary, and it is one side condition on one rule, not a convention anybody has to remember. Mitchell and Plotkin (1988) were the first to put it this way.

An honesty about the correspondence. The system just described is not an invention of these notes: it is the polymorphic $\lambda$-calculus, found twice, by Jean-Yves Girard in 1971 and by John Reynolds in 1974, and it is the core of every language with generics in it. Two things about it are worth keeping straight. Its $\forall$ and $\exists$ range over types, whereas the quantifiers of a specification range over the things a program handles — days, users, positions in a list — so the two are different quantifiers over different domains, and the logic whose proofs are polymorphic programs is a different and stronger one than the chapter builds. What is the same, exactly the same, is the four rules and their side conditions: a rule to instantiate, a rule to generalise that may not generalise a variable the context has fixed, a rule to package a witness, and a rule to unpack one that may not let the witness escape. Having seen them as type rules, you will recognise them in §4.3 on sight.

4.3 The quantifier rules

Chapter 3 gave each connective a rule that introduces it and a rule that eliminates it, and nothing else. The quantifiers get the same treatment, two rules each, and the four rules are the four moves of §4.2 written down.

Read the four against the compiler.

• ($\forall$E) is instantiation: a call. You have something that holds for every $x$; you use it at the $t$ in hand. The side condition is the one that stops $t$ being captured on the way in, and §4.3 is about what happens without it.
• ($\forall$I) is generalisation: a definition. You proved $A$ of a $y$ about which you assumed nothing, so you have proved it of everything. Assumed nothing is the side condition, and it says in the logic exactly what “rigid type variable” says in the compiler: $y$ may not be free in any hypothesis still in use.
• ($\exists$I) is building a module: supply the witness $t$ and the evidence $A(t∕x)$, and what comes out mentions neither. A proof of $\exists xA$ is the pair.
• ($\exists$E) is using one: from $\exists xA$ you may go on to anything you could have derived from $A(y∕x)$ for a fresh $y$. The three conditions on $y$ are the three ways of cheating, and together they say: you may use the thing, but you may not learn which thing it is. That is a module boundary, written as a side condition.

($=$I) says everything equals itself and ($=$E) is Leibniz’s law: equals may be substituted for equals in any claim. Symmetry and transitivity of $=$ are not rules because they follow from these two (Exercise 4.1).

Notice what is not here, and was in Chapter 2: a Deduction Theorem. There is nothing left for it to say. Its content — that anything provable on the supposition $A$ yields $A\to B$ without the supposition — is the rule ($\to$I), which this system simply has. Where Chapter 2 had to prove that supposing was safe, and pay for every supposition with instances of (II), natural deduction supposes and discharges as a matter of course. That is what makes the proofs below short enough to read.

Where the eigenvariable condition bites. The proviso on ($\forall$I) is worth one example of its own, because getting it wrong is a real class of bug and not a technicality. Suppose the policy is being checked for a particular user, and the hypothesis in use is $\mathrm{𝖺𝖽𝗆}(u)$: this user is an administrator. One application of ($\forall$I) would give $\forall x\mathrm{𝖺𝖽𝗆}(x)$: everyone is an administrator, from which, with the policy, everyone may read everything. The rule forbids it, and the condition is exactly the right one: $u$ is free in the hypothesis $\mathrm{𝖺𝖽𝗆}(u)$, which is still in use, so $u$ is not arbitrary. Discharge the hypothesis first, by ($\to$I), and generalisation becomes legal — but then what you have generalised is $\mathrm{𝖺𝖽𝗆}(u)\to \dots$, which is the harmless and true thing. Exercise 4.5 runs the bug to $\perp$.

Substitutability: the same bug twice. Rule ($\forall$E) lets you go from $\forall xA$ to $A(t∕x)$ — what holds of everything holds of $t$ — if $t$ is substitutable for $x$ in $A$. Drop the condition and the system proves $\perp$ from a specification any programmer would write. Let the one hypothesis be

“no element is the only element”, which is what you say of any collection with two things in it. Take $A$ to be $\neg \forall y(y=x)$ and $t$ to be the variable $y$, which is not substitutable for $x$ in $A$, since it would land under the $\forall y$; and pretend ($\forall$E) did not care.

1.

$\forall x\neg \forall y(y=x)$ hypothesis

2.

$\neg \forall y(y=y)$ the illegal ($\forall$E) on 1, $t:=y$

3.

$y=y$ ($=$I)

4.

$\forall y(y=y)$ ($\forall$I) on 3; $y$ is free in no hypothesis

5.

$\perp$ ($\to$E) 2, 4, since line 2 is $\forall y(y=y)\to \perp$

Five lines, and the system has proved $\perp$ from a harmless hypothesis: exactly the disaster Theorem 3.19 ruled out, and the only thing that let it happen was line 2. What went wrong is visible in the formulas. The $y$ we substituted meant “some given element”; on landing under $\forall y$ it came to mean “whichever $y$ the quantifier picks”. With the condition in force, line 2 is not available. The fix is to rename first: the hypothesis is equally well written $\forall x\neg \forall z(z=x)$, its legal instance at $y$ is $\neg \forall z(z=y)$, and nothing follows from that but what should.

You have met this bug, and not only in logic. It is variable capture, the bug that clause 5 of substitution in Chapter 3 exists to prevent. Running a program was substitution, $(\mathit{𝜆𝑥}.M)N⇝M(N∕x)$, and it needs the same condition. Take $\mathit{𝜆𝑥}.\mathit{𝜆𝑦}.x$ — $𝖪$, the function that keeps its first argument — applied to a free variable $y$, and run it blindly:

The free $y$ has landed under the inner $\mathit{𝜆𝑦}$ and been captured; the result is the identity, which returns whatever it is given, and the program’s meaning has changed. Rename first, $(\mathit{𝜆𝑥}.\mathit{𝜆𝑧}.x)y⇝\mathit{𝜆𝑧}.y$, and the constant function we meant comes out. On the proof side, with the free $y$ of type $B$ and the parameter of type $A$, the program before the step is a proof of $A\to B$ from the hypothesis $B$; the blind result $\mathit{𝜆𝑦}.y$ is a proof of $A\to A$ from nothing. Capture has swapped one theorem for another, which is what it did on the logic side too. One bug, one fix, on both sides of the correspondence; and a language implementation never substitutes text — it carries the argument’s value in an environment — which is why you have met the bug in macros and refactoring tools, which do, and not in function calls.

4.4 Derivations as trees

Definition 3.12 built derivations as trees for the connectives, and tracked for each one the set $\mathrm{OH}(𝒟)$ of hypotheses it still rests on. Four clauses extend it to the quantifiers, and the side conditions become easier to state when they are written this way, not harder — which is the reason for doing it.

The variable $y$ in clauses 11 and 13 is called the eigenvariable of the step, and it is the only thing in this chapter that needs care. Read the two conditions. What the condition says, and why the tree says it better. Clause 11 asks that $y$ be free in no open hypothesis of the subderivation. That is the exact sense of “$y$ was arbitrary”: nothing the derivation still leans on says anything about $y$ in particular, so whatever was shown of $y$ was shown of anything. Compare the list form, rule ($\forall$I) of Definition 4.6, which asks that $y$ be free in no formula of $\mathrm{\Gamma }$. That is sound, but it is coarser: $\mathrm{\Gamma }$ is whatever set the line happens to carry, and may include formulas the derivation never used. A tree carries exactly the hypotheses it needs, so the condition it states is exactly the condition that matters. This is the one place where the tree notation is not merely nicer to read but says something sharper, and it is why proof theory is written in trees.

Clause 13 has three conditions and each rules out one way of cheating.

• $y$ not free in $C$: you may not let the witness escape in the answer. “Some user can read the file; call them $y$; therefore $y$ can read the file” is not a valid step, because $y$ was a name you made up.
• $y$ not free in $\exists xA$: the fresh name must really be fresh, and not a variable the existential claim already mentions.
• $y$ not free in the other open hypotheses: nothing else in use may already say something about $y$.

Those three are the type-theoretic condition of (4.2) — the implementation type may be used inside the match and may not leave it — translated word for word, with $y$ for the type variable $a$. Compare them against the rule ($\exists$E) you have already read on page 138: a derivation that breaks one of them is a program that GHC rejects with rigid type variable would escape its scope.

The policy, as trees. Here is the access-control policy of §4.1 at work. Write

— administrators may read anything, and owners are administrators — and suppose we are also told $\mathrm{𝖺𝖽𝗆}(\mathrm{𝖺𝗅𝗂𝖼𝖾})$. Can Alice read the config file? Two instantiations and one application:

Three bars; the open hypotheses are the one policy line and the one fact, so the tree witnesses ${\mathrm{\Gamma }}_{\mathrm{pol}}\cup \{\mathrm{𝖺𝖽𝗆}(\mathrm{𝖺𝗅𝗂𝖼𝖾})\}⊢\mathrm{𝗋𝖾𝖺𝖽}(\mathrm{𝖺𝗅𝗂𝖼𝖾},\mathrm{𝖼𝖿𝗀})$. It is a certificate: an auditor who disbelieves the answer need not rerun the system, and need not understand it either. They check three bars.

Now something no policy engine can settle by evaluation, because it quantifies over all users and all resources at once: from ${\mathrm{\Gamma }}_{\mathrm{pol}}$, every owner may read what they own. Let $𝒟$ be the derivation that puts the two policy lines together on a supposition $\mathrm{𝗈𝗐𝗇}(u,v)$ — four instantiations and two applications, the moves just used — ending in $\mathrm{𝗋𝖾𝖺𝖽}(u,v)$.

The supposition ${[\mathrm{𝗈𝗐𝗇}(u,v)]}^1$ sits at a leaf of $𝒟$ and is discharged at the first bar. Only then are the two generalisations legal, and now you can check that against clause 11 rather than take it on trust: after the discharge, $\mathrm{OH}$ of the subderivation is just the two policy lines, and both are sentences, so neither $v$ nor $u$ is free in any of them. Had we generalised before discharging, $\mathrm{𝗈𝗐𝗇}(u,v)$ would still have been open, $v$ would have been free in it, and the clause would not have applied — which is the formal version of the complaint that we were claiming the policy for all users on the strength of one.

A proof of there is names the thing. One more, and it is the one that pays. From the same policy and $\mathrm{𝖺𝖽𝗆}(\mathrm{𝖺𝗅𝗂𝖼𝖾})$, one more bar on the first tree gives

somebody can read the config file. Read as a program, the step packs the witness $\mathrm{𝖺𝗅𝗂𝖼𝖾}$ together with the evidence that she qualifies. And that packing is not a convenience of the notation: in this logic it is the only way an $\exists$ can be introduced, which has a consequence worth stating.

That property is exactly what an audit wants. “Is this file readable by anyone outside the team?” is an existence question, and an answer of yes that cannot say who is no use to a security engineer. In this logic every yes comes with the name attached.

It is also strong enough to be worth distrusting. “Either the program halts or it does not” is the kind of thing one would like to assert without producing either a halting run or a proof that there is none; “some input breaks this function” is the kind of thing one would like to assert without producing the input. In the logic of these four chapters you may assert neither. Whether that is a virtue or a restriction is a question we cannot yet ask, because asking it needs the word Part 2 supplies.

4.5 Sorting, and what its type cannot say

Here is insertion sort, written so that the comparison is a parameter — which is how every sorting routine in every standard library is written, because the library cannot know what you are sorting.

sort(lt, xs): 
    out = [] 
    for x in xs: 
        i = 0 
        while i < length(out) and lt(out[i], x): 
            i = i + 1 
        insert x into out at position i 
    return out

Everything in this part applies to that program. It has a type, and the type is polymorphic in the sense of §4.2:

one program for every element type, instantiated by ($\forall$E) at each call. The checker proves that type, and by Chapter 3 the proof is the program. So the compiler has certified something real: this code will not add a string to a number, will not call a non-function, and will hand back a list of the type it was given.

It has certified nothing whatever about sorting.

The gap is the parameter lt. Give sort a comparison that returns True whenever the two arguments are equal — <= where < was meant, the single commonest mistake in the business — and the type is unchanged, because <= and < have the same type. The program compiles, runs, and returns a list; the list is sometimes not sorted; and on a longer input the routine may do something stranger. This is the exception Java’s sort really throws:

Read it carefully, because it is unusual and exact. The sort has not checked the contract — checking it would need every pair of elements, which costs more than the sort. What it has noticed is that its own bookkeeping has become impossible: it merged two runs it had recorded as ordered and found them not ordered, which cannot happen if the comparison behaves. It detected the failure of a consequence of the contract. To say what that means, we have to be able to state the contract and derive the consequence, and neither is possible in a type.

The contract. What sort needs of lt is that it be a strict total order: three sentences, in the language of §4.1, with $x<y$ for lt(x,y).

Call those three $\mathrm{\Gamma }$. They say for all, so no type can hold them; they are about the elements, so Chapter 3 could not write them; and they are what the library’s documentation is trying to say in English. Now the consequence. What a comparator built from <= violates is asymmetry: it reports $a<b$ and $b<a$ for a pair of equal elements, and no comparator obeying the contract can.

That is not one of the three sentences, so it has to be derived. Informally the argument is one line: if $u<v$ and $v<u$ then by transitivity $u<u$, which irreflexivity forbids. The derivation makes each of those words a step. Write $\mathrm{\Delta }$ for $\mathrm{\Gamma }$ together with the supposition $u<v\wedge v<u$.

1.

$\mathrm{\Delta }⊢u<v\wedge v<u$ (hyp), the supposition

2.

$\mathrm{\Delta }⊢\forall x\forall y\forall z(x<y\wedge y<z\to x<z)$ (hyp), transitivity

3.

$\mathrm{\Delta }⊢\forall y\forall z(u<y\wedge y<z\to u<z)$ ($\forall$E) on 2, $t:=u$

4.

$\mathrm{\Delta }⊢\forall z(u<v\wedge v<z\to u<z)$ ($\forall$E) on 3, $t:=v$

5.

$\mathrm{\Delta }⊢u<v\wedge v<u\to u<u$ ($\forall$E) on 4, $t:=u$

6.

$\mathrm{\Delta }⊢u<u$ ($\to$E) 5, 1

7.

$\mathrm{\Delta }⊢\forall x\neg (x<x)$ (hyp), irreflexivity

8.

$\mathrm{\Delta }⊢\neg (u<u)$ ($\forall$E) on 7, $t:=u$

9.

$\mathrm{\Delta }⊢\perp$ ($\to$E) 8, 6

10.

$\mathrm{\Gamma }⊢\neg (u<v\wedge v<u)$ ($\to$I) 9, discharging the supposition

11.

$\mathrm{\Gamma }⊢\forall y\neg (u<y\wedge y<u)$ ($\forall$I) on 10

12.

$\mathrm{\Gamma }⊢\forall x\forall y\neg (x<y\wedge y<x)$ ($\forall$I) on 11

Read it in four blocks. Lines 2–5 strip the three quantifiers off transitivity, choosing $t:=u$ at the last step; that is the step that says “then $u<u$”. Line 6 fires it on the supposition. Lines 7–9 strip irreflexivity and reach $\perp$. Line 10 discharges, which is what turns “the supposition leads to absurdity” into “the supposition is false”, and lines 11–12 generalise. Both generalisations satisfy the side condition, and now you can say exactly why: after line 10 the hypotheses in use are the three contract sentences, and a sentence has no free variables, so neither $u$ nor $v$ is free in any of them.

Two things about the shape of that derivation are worth having. The supposition did all the work: there is no axiom in it anywhere and no theorem imported from elsewhere, because ($\to$I) lets the derivation suppose and then pay for the supposition. Chapter 2 could not do that. In its system the same fact needed contraposition proved separately and brought in as a line, and it needed the Deduction Theorem to license the supposition at all; here supposing is a rule, and that is the whole difference the move to natural deduction bought. The second thing is that every line is checkable by pattern matching against (4.3), side conditions included, so the twelve lines are a certificate in the sense this part has used throughout.

So: a comparator obeying the contract can never report both $a<b$ and $b<a$. When the sort catches a comparator doing exactly that, the exception is reporting a theorem being violated — a theorem the type checker could not state, let alone prove, and that a verifier, which is a type checker whose types may quantify, could. That is the whole distance between safe and correct, measured on a program you have called a hundred times.

4.6 Checking is easy; finding is not

We can now write down the question “does $A$ follow from the specification $\mathrm{\Gamma }$?”, and when the answer is yes a derivation exists. It is tempting to conclude that we have an algorithm for the question: to decide it, “just” check whether a derivation exists.

Because you do not know how long a derivation of $A$, if there is one, might be. Suppose you knew a bound: that whenever $A$ follows from $\mathrm{\Gamma }$ at all, it does so by a derivation of at most a thousand symbols. Then you could enumerate the finitely many strings of at most that length and check each, and the rules of (4.3) would do the rest. (A bound on the number of lines would not do: each line can be as long as you like.) But no such bound is known, and a search that has not found a derivation yet cannot tell whether to give up. What we have is a checker for certificates and no finder. This is the point at which the ambition of the next part declares itself. If a proof can be checked mechanically, why can it not be found mechanically? Mathematics would then be a thing one could automate: state the specification, state the claim, and let the machine report. That programme is not a fantasy and it is not finished, and Part 2 is largely about how far it goes. The short answer is that it goes further than you would guess and stops sooner than Hilbert hoped.

Your compiler, meanwhile, is in exactly the position we are in: it checks the proof your program is; it does not find one. You have, by now, tools that will hand you a program of a type you name, or a patch for a bug you describe, and what they hand you is a candidate. The compiler’s check is what makes a candidate more than a guess, and when the type can say for all, the check is a verification against the specification. Finding has become cheap; checking is what is left to trust, and it is the subject of this course.

A specification is a set of sentences — three lines of a comparator contract, two lines of an access-control policy, whatever a sale is — and “$A$ follows from the specification” is a precise, checkable claim. The language that states it is first-order logic (Definition 4.1); the rules that certify it are Gentzen’s, four of them for the quantifiers (Definition 4.6), and they are the compiler’s two moves for a polymorphic type and its two ways with a module, side conditions and all. A proof of an $\exists$ hands back the witness it was built with (Remark 4.8). A type checker certifies that a program is safe to run. A verifier — a type checker whose types may say for all — certifies that it is correct, meaning: the postcondition is provable from the precondition and the specification. The discount patch is correct or not according to three or four sentences about sales, and once they are written down the question has an answer a checker can verify.

Checking is easy. Finding is not. Proof checking is pattern matching, and it is what your compiler does; proof finding, so far, is cleverness. Three questions about any proof system. Could it prove something false? — we have shown that this one does not prove everything (Theorem 3.19), which is all that “false” can mean until the word has a meaning. Does it prove everything it should? — we cannot even ask. Can the search for a proof be made mechanical, an algorithm and not a genius? — not yet. And a puzzle to take into next week. Peirce’s law,

is a formula built from letters and arrows like any other. Try to write a program of that type before next week. You will not manage, and nothing in this part can tell you whether that is your fault or the formula’s. Part 2 begins by giving the formulas a meaning, and the first thing it finds out is what Peirce’s law is.

Exercises

Reading

Girard et al. (1989, chapters 2–4) again, for natural deduction with quantifiers and the normalisation theorem Remark 4.8 borrows; Open Logic Project (2026, chapter 13) for the same rules at more leisure, and for the Hilbert-style presentation this chapter did not need. Mitchell and Plotkin (1988) for modules as existentials. Next, Part 2: what the formulas mean, and what that reveals about the logic this part has been using. References.