§1. Introduction. For most of its history, mathematics was algorithmic in nature. The geometric claims in Euclid's Elements fall into two distinct categories: “problems,” which assert that a construction can be carried out to meet a given specification, and “theorems,” which assert that some property holds of a particular geometric configuration. For example, Proposition 10 of Book I reads “To bisect a given straight line.” Euclid's “proof” gives the construction, and ends with the (Greek equivalent of) Q.E.F., for quod erat faciendum, or “that which was to be done.” Proofs of theorems, in contrast, end with Q.E.D., for quod erat demonstrandum, or “that which was to be shown”; but even these typically involve the construction of auxiliary geometric objects in order to verify the claim.

Similarly, algebra was devoted to developing algorithms for solving equations. This outlook characterized the subject from its origins in ancient Egypt and Babylon, through the ninth century work of al-Khwarizmi, to the solutions to the quadratic and cubic equations in Cardano's Ars Magna of 1545, and to Lagrange's study of the quintic in his Réflexions sur la résolution algébrique des équations of 1770.

The theory of probability, which was born in an exchange of letters between Blaise Pascal and Pierre de Fermat in 1654 and developed further by Christian Huygens and Jakob Bernoulli, provided methods for calculating odds related to games of chance.

§1. Computer calculation.

1.1. A panorama of the status quo. Where stands the mathematical endeavor?

In 2012, many mathematical utilities are reaching consolidation. It is an age of large aggregates and large repositories of mathematics: the arXiv, Math Reviews, and euDML, which promises to aggregate the many European archives such as Zentralblatt Math and Numdam. Sage aggregates dozens of mathematically oriented computer programs under a single Python-scripted front-end.

Book sales in the U.S. have been dropping for the past several years. Instead, online sources such as Wikipedia and Math Overflow are rapidly becoming students' preferred math references. The Polymath blog organizes massive mathematical collaborations. Other blogs organize previously isolated researchers into new fields of research. The slow, methodical deliberations of referees in the old school are giving way; now in a single stroke, Tao blogs, gets feedback, and publishes.

Machine Learning is in its ascendancy. Log Answer and Wolfram Alpha answer our elementary questions about the quantitative world; Watson our Jeopardy questions.

§1. Introduction. In recent years there has emerged the study of discrete computational models which are allowed to act transfinitely. By ‘discrete’ we mean that the machine models considered are not analogue machines, but compute by means of distinct stages or in units of time. The paradigm of such models is, of course, Turing's original machine model. If we concentrate on this for a moment, the machine is considered to be running a program P perhaps on some natural number input n ∈ ℕ and is calculating P(n). Normally we say this is a successful computation if the machine halts after a finite number of stages and we may read off some designated form of output: ‘P(n)↓’ However if the machine fails to halt after a finite time it may be exhibiting a variety of behaviours on its tape. Mathematically we may ask what happens ‘in the limit’ as the number of stages approaches ω. The machine may of course go haywire, and simply be rewriting a particular cell infinitely often, or else the Read/Write head may go ‘off to infinity’ as it moves inexorably down the tape. These kind of considerations are behind the notion of ‘computation in the limit’ which we consider below.

Or, it may only rewrite finitely often to any cell on the tape, and leave something meaningful behind: an infinite string of 0, Is and thus an element of Cantor space 2ℕ. What kind of elements could be there?

Abstract. In §1 we give a short overview for a general audience of Godel, Church, Turing, and the discovery of computability in the 1930s. In the later sections we mention a series of our previous papers where a more detailed analysis of computability, Turing's work, and extensive lists of references can be found. The sections from §2—§9 challenge the conventional wisdom and traditional ideas found in many books and papers on computability theory. They are based on a half century of my study of the subject beginning with Church at Princeton in the 1960s, and on a careful rethinking of these traditional ideas.

The references in all my papers and books are given in the format, author [year], as in Turing [1936], in order that the references are easily identified without consulting the bibliography and are uniform over all papers. A complete bibliography of historical articles from all my books and papers on computabilityis given on the page as explained in §10.

§1. A very brief overview of computability.

1.1. Hilbert's programs. Around 1880 Georg Cantor, a German mathematician, invented naive set theory. A small fraction of this is sometimes taught to elementary school children. It was soon discovered that this naive set theory was inconsistent because it allowed unbounded set formation, such as the set of all sets. David Hilbert, the world's foremost mathematician from 1900 to 1930, defended Cantor's set theory but suggested a formal axiomatic approach to eliminate the inconsistencies. He proposed two programs.

Synopsis: To prove soundness of the Verifiable C separation logic, we first give a model of mpred as pred(rmap), that is, predicates on resource maps. We give a model for permission-shares using trees of booleans. We augment the C light operational semantics with juicy memories that keep track of resources as well as “dry” values. We give a semantic model of the Hoare judgment, using the continuation-passing notion of “guards.” We use this semantic model to prove all the Hoare rules. Our model and proofs have a modular structure, so that they can be ported to other programming languages (especially in the CompCert family).

Synopsis: Indirection theory gives a clean interface to higher-order step indexing. Many different semantic features of programming languages can be modeled in indirection theory. The models of indirection theory use dependent types to stratify quasirecursive predicates, thus avoiding paradoxes of self-reference. Lambda calculus with mutable references serves as a case study to illustrate the use of indirection theory models.

When defining both Indirection and Separation one must take extra care to ensure that aging commutes over separation. We demonstrate how to build an axiomatic semantics with using higher-order separation logic, for the pointer/continuation language introduced in the case study of Part II.

In a conventional separation logic we have a “maps-to” operator a ↦ b saying that the heap contains (exactly) one cell at address a containing value b. This operator in the separation logic corresponds to the load and store operators of the operational semantics.

Now consider two more operators of an operational semantics: function call and function definition. When function names are static and global, we can simply have a global table relating functions to their specifications—where a specification gives the function's precondition and postcondition. But when the address of a function can be kept in a variable, we want local specifications of function-pointer variables, and ideally these local specifications should be as modular as the rest of our separation logic. For example, they should satisfy the frame rule. That is, we might like to write assertions such as (a ↦ b) * (f : {P}{Q}) meaning that a is a memory location containing value b, and a different address f is a function with precondition P and postcondition Q. Furthermore, the separation * guarantees that storing to a will not overwrite the body of f.

To illustrate these ideas in practice, we will consider a tiny programming language called Cont. The functions in this language take parameters f(x, y, z) but they do not return; thus, they are continuations.

Indirection theory is a powerful technique for using step-indexing in modeling higher-order features of programming languages. Rmaps (Chapters 39 and 40), which figure prominently in our model of Verifiable C, rely heavily on indirection theory to express self-reference.

When reasoning in a program logic, step indexes are unproblematic: the step indexes can often be hidden via use of the ▹ operator, and therefore do not often appear explicitly in assertions. Indirection theory provides a generic method for constructing the underlying step-indexed models.

More problematic is how to connect a step-indexed program logic like Verifiable C to a certified compiler such as CompCert. CompCert's model of state is not step-indexed, nor would it be reasonable to make CompCert step-indexed. To do so introduces unnecessary complication into CompCert's correctness proofs. It also complicates the statement of CompCert's correctness theorem: naively requiring the compiler to preserve all step indexes through compilation makes it difficult to reason about optimizations that change the number of steps.

Previous chapters of this book outlined one way in which this difficulty can be resolved, by stratifying our models into two layers: operational states corresponding to states of the operational semantics used by CompCert, and semantic worlds appearing in assertions of the program logic. Chapter 40 in particular gave some motivation for why this stratification makes sense: We may not want all the information found in operational states to be visible to Hoare logic assertions (in particular, control state should be hidden).

CompCert defines a formal small-step operational semantics for every intermediate language (including C light) between C and assembly language.

For Verifiable C, we use the C light syntax with an alternate (non-standard) operational semantics of C light (file veric/Clight_new.v). Our nonstandard semantics is quite similar to the standard, but it makes fewer “administrative small-steps” and is (in this and other ways) more conducive to our program-logic soundness proof. We prove a simulation relation from our alternate semantics to the CompCert standard C light semantics. This ensures that the soundness we prove relative to the alternate semantics is also valid with respect to the standard semantics.

In our operational semantics, an operational state is either internal, when the compiled program is about to execute an ordinary instruction of a single C thread; or external, when the program is requesting a system call or other externally visible event.

An internal operational state contains:

genv Global environment, mapping identifiers to addresses of global (extern) variables and functions, and a separate mapping of function-addresses to function-bodies.

ve Variable environment, mapping identifiers to addresses of addressable local variables—those to which the C-language & (address-of) operator is somewhere applied.

te Temp environment, mapping identifiers to values of ordinary local variables—those to which & is never applied.

k Continuation, representing the stack of control and data (including the program counter, return addresses for function calls, and local variables of suspended functions).

Program logics for certified compilers: We prove that the program logic is sound with respect to the operational semantics of a source language—meaning that if the program logic proves some claim about the observable behavior of a program, then the source program actually respects that claim when interpreted in the source-language semantics. But computers don't directly execute source-language semantics: we also need a proof about the correctness of an interpreter or a compiler.

CompCert (compilateur certifié in French) is a formally verified optimizing compiler for the C language, translating to assembly language for various machines (Intel x86, ARM, PowerPC) [62]. Like most optimizing compilers, it translates in several sequential phases through a sequence of intermediate languages. Unlike most compilers, each of these intermediate languages has a formal specification written down in Coq as an operational semantics. Each phase is proved correct: the form of the proof is a simulation theorem expressing that the observable behavior of the target program corresponds to the observable behavior of the source program. The composition of all these per-phase simulation theorems gives the compiler correctness theorem.

Although there had been formally verified compilers before [67, 36, 61, 60], CompCert is an important breakthrough for several reasons: