This article shows that theory exploration arises naturally from the need to progressively modify applied formal theories, especially those underpinning deployed systems that change over time or need to be attack-tolerant. Such formal theories require us to explore a problem space with a proof assistant and are naturally dynamic. The examples in this article are from our on-going decade-long e ort to formally synthesize critical components of modern distributed systems. Using the Nuprl proof assistant we created event logic and its protocol theories. I also mention the impact over this period of extensions to the constructive type theory implemented by Nuprl. One of them led to our solution of a long standing open problem in constructive logic. Proof exchange among theorem provers is promising for improving the \super tactics" that provide domain speci c reasoners for our protocol theories. Both theory exploration and proof exchange illustrate the dynamic nature of applied formal theories built using modern proof assistants. These activities dispel the false impression that formal theories are rigid and brittle artifacts that become less relevant over time in a fast moving eld like computer science.
I believe that one of the major scienti c accomplishments of computer science is the creation
of software systems that provide indispensable help in performing complex reasoning tasks
and in automating abstract intellectual processes. Among such systems are proof assistants.
They have helped people solve open mathematical problems, build provably correct hardware
and software, create attack-tolerant distributed systems, and implement foundational theories
of mathematics and computer science. These assistants are also nding a place in advanced
technical education [
These accomplishments with proof assistants are well documented in academic journals and
con rmed by industrial uptake. Nevertheless, many otherwise well-informed and in uential
scientists believe that proof assistants are very di cult to use in these ways and that their
solutions are expensive, rigid, and in exible [
The fact that we can easily modify, reuse, and replay formal theories might be the main driving force spreading their widening use, just as it is a driving force in the universal spread of text editors, compilers, programming environments, and other commonly used \tools for precise thought". I predict that we will see in the near future dynamic formal theories that are developed and maintained by a community of researchers using proof assistants to support applied formal theories that in turn support deployed software systems \on the y". We already see communal activity in joint e orts to build mathematical theories or settle open problems, and that is a rst step. 1.1
I explain these claims by referring to proof assistants that implement constructive type theories
{ because these are the proof assistants I know best and because they also connect directly to
programming practice. Indeed, they support what has come to be called correct-by-construction
programming and formal system evolution [
I mention brie y just one example of the gradual extension of Constructive Type Theory
(CTT), the theory implemented by Nuprl. This example led my colleague Mark Bickford and
me to solve an open problem in logic by nding a completeness theorem for intuitionistic
rstorder logic [
Additions to the underlying foundational type theory can be indexed by the years in which they were made, up to the one we used to solve the problem, say from CTT00 to CTT10. The base theory is CTT84, and we are now using CTT12.1 By and large each theory is an extension of the previous one, although there was a major improvement from CTT02 onwards along with a corresponding change in the proof assistant from Nuprl4 to Nuprl5.
In the special case of proof assistants based on the LCF tactic mechanism [
These scienti c contributions are enabled by a powerful and ubiquitious information technology that integrates programming languages, interactive provers, automatic provers, model checkers, and databases of formal knowledge. I believe that this integrated technology is rapidly moving toward a point at which it will provide tools for thought able to accelerate scienti c research and enrich education in ways computer scientists have only imagined before. The practical integration of computing and logic seen for the rst time in this research area has made us aware in detail that there is a computational reality to logic which Turning glimpsed in general outline in 1936.
1In contrast, I believe that the formalized Tarski-Grothendieck set theory used by the Mizar system [
According to Andrew Hodges [
Turing also made the notion of a computable function a central concept in science. This in turn made the notion of data types fundamental and linked them to Russell's conception of a type. Now we see types in the curriculum from the school level through university education. Sets are taught in mathematics, types in programming. In modern type theory, we see sets (in their in nite variety) as a special data type that appeals to mathematicians. So we take a brief historical look at types to explain their use in proof assistants.2 1.3
The notion of type is a central organizing concept in the design of programming languages,
both to de ne the data types and also to determine the range of signi cance of procedures
and functions.3 Types feature critically in reasoning about programs as Hoare noted in his
fundamental paper on data types [
Type theory serves as the logical language of several interactive theorem provers including
Agda [
The gap between data types in programming languages and those in foundational type theory and from there to constructive type theory are large. That rst gap can be traced to the in uence of Principia Mathematica and the second to the in uence of the mathematician L.E.J. Brouwer 2I wrote a longer unpublished paper in 2010 for the 100 year anniversary of Principia Mathematica entitled \The Triumph of Types: Principia Mathematica's Impact on Computer Science". It describes the in uence of type theory on computer science and is available at the celebration web page. These notes rephrase a few examples used there.
3This use matches Russell's de nition of a type as the range of signi cance of a propositional function. and his intuitionistic program for mathematics. We look very brie y at these historical gaps to establish the context for the work of modern proof assistants supporting applied formal theories and correct-by-construction programming. 2.1
Near the turn of the last century, Frege [
For Russell and Whitehead, type theory was not introduced because it was interesting on
its own, but because it served as a tool to make logic and mathematics safe. According to
PM page 37: Type theory \only recommended itself to us in the rst instance by its ability
to solve certain contradictions. ... it has also a certain consonance with common sense which
makes it inherently credible". This common sense idea was captured in Russell's de nition of
a type in his Principles of Mathematics, Appendix B The Doctrine of Types [
According to PM, statements of pure mathematics are inferences of pure logic. All commitments to \reality" (Platonic or physical) such as claims about in nite totalities, the interpretation of implication as a relation, the existence of Euclidean space, etc. were taken as hypotheses. At the time of PM it appeared that there would emerge settled agreement about the nature of pure inferences and their axiomatization. That was not to be. Even the notion of pure logic would change. 2.2
While Russell was working on his theory of types [
This line of research eventually led to two extensional type theories, Intuitionistic Type
Theory (ITT82, ITT84) [
Computational content is present in the provable assertions of the constructive type theories,
and one of the features of CIC, CTT, and ITT is that implementing the proof machinery makes it
possible to extract this content and execute it. This discovery has led to a new proof technology
for extracting computational content from assertions. That technology has proven to be very
e ective in practice, where it is called correct-by-construction programming. There is a growing
literature on this subject with references in survey articles such as [
Brouwer's notion of computability was not formal and not axiomatic. It was intuitive and corresponds to what is called e ective computability. The Church/Turing Thesis claims that all e ectively computable functions are computable by Turing machines (or any equivalent formalism, e.g. the untyped -calculus). There is no corresponding formalism for Brouwer Computable. However, I believe that this notion can be captured in intuitionistic logics by leaving a Turing complete computation system for the logic open-ended in the sense that new primitive terms and rules of reduction are possible. This method of capturing e ective computability may be unique to CTT in the sense that the computation system of CTT is open to being \Brouwer incomplete" as a logic. We have recently added a primitive notion of general process to formalize distributed systems whose potentially nonterminating computations are not entirely e ective because they depend on asynchronous message passing over a network which can only be modeled faithfully by allowing unpredictable choices by the environment, e.g. the internet. 3
The PRL group's most practical results in formal methods might be the optimization of protocol
stacks [
Based on our work in this area, we came to see that writing correct distributed protocols was an extremely di cult business. Basically no one can write these protocols completely correctly \by hand", so they are all gradually debugged in the eld. This became an excellent target on which to deploy formal methods, in particular correct-by-construction programming. To start this we needed a speci cation language for distributed system behavior. We noticed that our collaborators used message sequence diagrams as their main informal method of description and reasoning. They did not use temporal logic in any form, they did not use any process algebra, they did not use a logic of actions. So we decided to create a logic that matched their way of thinking as closely as possible. As we spoke it with them, it gradually evolved. The tools of the Nuprl proof assistant and its Logical Programming Environment greatly aided that evolution in ways that I will explain as an example of theory exploration in action. 3.1
The interested reader could track the evolution of the logic of events from the rst publications
in 2003 to the latest publications in 2012, [
In A Logic of Events [
We learned that the key axiom for many proofs was that causal ordering [
By 2010 we could automatically generate proofs from the higher level event classes to the
lowest level process code, now implemented in our new programming interface to Nuprl built
4This style has the unintended consequence of citing a very large number of our own papers.
by Vincent Rahli called EventML [
During the period from 2005 to 2009 we learned to modify and extend the entire theory step by step and replay all the proofs. Mark Bickford and Richard Eaton developed mechanisms to replay the proofs, nd the broken steps, and modify the tactics and then replay the entire event theory library.
I can only cover one point of this long and rich technical story in this short article. We turn
to that one point next. In due course we will publish more \chapters" of the story now that
we have deployed our synthesized consensus protocols in a working system called ShadowDB
and have started collecting data about its performance [
We now look brie y at how our understanding of causal order changed as the theories evolved. The same kind of story could be told about minimizing the role of state, about the need for event combinators, and about the need for sub-processes that live only for short periods. All of this would take a monograph. So I will focus on only one such aspect.
Lamport discovered in 1978 that causal order was the right notion of time in distributed
systems [
To show that causal order is well-founded, we notice that in any execution of a distributed system given by reduction rules, we can conduct a \tour of the events" and number them so that events caused by other events have a higher number. Thus causal order is well founded and if equality of events is decidable, then so is causal order. We show this below. 3.3.1
The signature of these events requires two types, and two partial functions. The types are discrete, which means that their de ning equalities are decidable. We assume the types are disjoint. We de ne D as fT : T ype j 8x; y : T: x = y in T _ : (x = y in T )g, the large type of discrete types.
E: D Loc:D pred?: E ! E + Loc sender?: E ! E + U nit
The function pred? nds the predecessor event of e if e is not the rst event at a locus or it returns the location if e is the rst event. The sender?(e) value is the event that sent e if e is a receive, otherwise it is a unit. We can de ne the location of an event by tracing back the predecessors until the value of pred belongs to Loc. This is a kind of partial function on E. From pred? and sender? we can de ne these Boolean valued functions:
f irst(e) = if is left (pred?(e)) then true else false rcv?(e) = if is left (sender?(e)) then true else false The relation is left applies to any disjoint union type A + B and decides whether an element is in the left or right disjunct. We can \squeeze" considerable information out of the two functions pred? and sender?. In addition to rst and rcv?, we can de ne the order relation pred!(e; e0) == (: f irst(e0) ) e = pred?(e0)) _ e = sender(e0):
The transitive closure of pred! is Lamport's causal order relation denoted e < e0: We can prove that it is well-founded and decidable; rst we de ne it.
The nth power of relation R on type T , is de ned as xRoy i x = y in T xRny i 9z : T: xRz & zRn 1y The transitive closure of R is de ned as xR y i 9n : N+:(xRny):
Causal order is x pred! y; abbreviated x < y. 3.3.2
There are only three axioms that constrain event systems with order beyond the typing constraints.
Axiom 1. If event e emits a signal, then there is an event e0 such that for any event e00 which receives this signal, e00 = e0 or e00 < e0.
8e : E:9e0 : E: 8e00 : E: (rcv?(e00) & sender?(e00) = e) ) (e00 = e0 _ e00 < e) Axiom 2. The pred? function is injective.
8e; e0 : E: loc(e) = loc(e0) ) pred?(e) = pred?(e0) ) e = e0 Axiom 3. The pred! relation is strongly well founded.
9f : E ! N: 8e; e0 : E:pred!(e; e0) ) f (e) < f (e0)
To justify f in Axiom 3 we arrange a linear \tour" of the event space in any computation. We imagine that space as a subset of N N where N numbers the locations and discrete time. Events happen as we examine them on this tour, so a receive can't happen until we activate the send. Local actions are linearly ordered at each location. Note, we need not make any further assumptions.
We can de ne the nite list of events before a given event at a location, namely before(e) == if rst(e) then[] else pred?(e) append before (pred? (e)) prior(e) == if rst(e) then[] else if rcv?(e) then < e; prior(sender?(e)); prior(pred?(e)) > else < e; prior(pred?(e)) >
Similarly, we can de ne the nite tree of all events causally before e, namely
We can prove many interesting facts about events with order. The basis for many of the proofs is induction over causal order. We prove this by rst demonstrating that causal order is strongly well founded.
Theorem 3.1. 9f : E ! N: 8e; e0 : E: e < e0 ) f (e) < f (e0)
The argument is simple. Let x y denote pred!(x; y) and let x n y denote pred!n(x; y): Recall that x n+1 y i 9z : E: x z & z n y: From Axiom 3 there is function fo : E ! N such that x y implies fo(x) < fo(z): By induction on N we know that fo(z) < fo(y): From this we have fo(x) < fo(y): So the function fo satis es the theorem. The simple picture of the argument is x z1 z2 : : : zn
y fo(x) < fo(z1) < : : : < fo(zn) < fo(y):
We leave the proof of the following induction principle to the reader.
Theorem 3.2. 8P : E ! P rop: 8e0 : E: ((8e : E: e < e0: P (e)) ) P (e0)) ) 8e : E: P (e)
Using induction we can prove that causal order is decidable.
Theorem 3.3. 8e; e0 : E: e < e0 _ : (e < e0)
We need the lemma.
Theorem 3.4. 8e; e0 : E: (e e0 _ : (e
e0))
This is trivial from the fact that pred!(x; y) is de ned using a decidable disjunction of decidable relations, recall x
y is pred!(x; z) so and
pred!(x; y) = : f irst(y) ) x = pred?(y) _ x = sender?(y): The local order given by pred? is a total order. De ne x <loc y is x = pred?(y): Theorem 3.5. 8x; y : E: (x <loc y _ x = y _ y <loc x)
The environment as well as the processes are players in the execution, determining whether protocols converge or not and whether they converge su ciently fast. However, unlike the processes, the environment is not a Turing computable player. It's behavior was not lawlike. This means that the reduction rule semantics should not be taken as the whole story, and the justi cation of causal order based on the computations is not the fundamental explanation, only a suggestive approximation. The best explanation are the axioms that de ne what the environment can contribute, and the induction principle on causal order. 3.4
Here is a brief overview of our General Process Model circa 2010 [
The internal part of a component is a process|its program and internal (possibly hidden) state. The external part of a component is its interface with the rest of the system. In this account, the interface will be a list of messages, containing either data or processes, labeled with the location of the recipient. The \higher order" ability to send a message containing a process allows a system to grow by \forking" or \bootstrapping" new components.
A system executes as follows. At each step, the environment may choose and remove a message from the external component. If the chosen message is addressed to a location that is not yet in the system, then a new component is created at that location, using a given boot-process, and an empty external part. Each component at the recipient location receives the message as input and computes a pair that contains a process and an external part. The process becomes the next internal part of the component, and the external part is appended to the current external part of the component.
A potentially in nite sequence of steps, starting from a given system and using a given
boot-process, is a run of that system. From a run of a system we derive an abstraction of its
behavior by focusing on the events in the run. The events are the pairs, hx; ni, of a location and
a step at which location x gets an input message at step n, i.e. information is transferred. Every
event has a location, and there is a natural causal-ordering on the set of events, the ordering
rst considered by Lamport [
We have found that requirements for distributed systems can be expressed as (higher-order) logical propositions about event-orderings. To illustrate this and motivate the results in the rest of the paper we present a simple example of consensus in a group of processes. Example 1. A simple consensus protocol: TwoThirds
Each participating component will be a member of some groups and each group has a name, G. A message hG; ii from the environment to component i informs it that it is in group G. The groups have n = 3f + 1 members, and they are designed to tolerate f failures. When any component in a group G receives a message h[start ]; Gi it starts the consensus protocol whose goal is to decide on values received by the members from clients. We assume that once the protocol starts, each process has received a value vi or has a default non-value.
The simple TwoThirds consensus protocol is this: A process Pi that has a value vi of type T starts an election to choose a value of type T (with a decidable equality) from among those received by members of the group from clients. The elections are identi ed by natural numbers, eli initially 0, and incremented by 1, and a Boolean variable decidei is initially f alse. The function from lists of values, Msg i to a value is a parameter of the protocol. If the type T of values is Boolean, we can take f to be the majority function.
Until decidei do: 1. Increment eli; 2. Broadcast vote heli; vii to G; 3. Collect in list Msg i 2f + 1 votes of election eli; 4. Choose vi := f (Msg i); 5. If Msg i is unanimous then decidei := true End
We describe protocols like this by classifying the events occurring during execution. In this algorithm there are Input, Vote, Collect, and Decide events. The components can recognize events in each of these event classes (in this example they could all have distinctive headers), and they can associate information with each event (e.g. hei; vii with Vote, Msg i with Collect, and f (Msg i) with Decide). Events in some classes cause events with related information content in other classes, e.g. Collect causes a Vote event with value f (Msg i).
In general, an event class X is function on events in an event ordering that e ectively partitions events into two sets, E(X) and E E(X), and assigns a value X(e) to events e 2 E(X).
Example 2. Consensus speci cation
Let P and D be the classes of events with headers propose and decide, respectively. Then the safety speci cation of a consensus protocol is the conjunction of two propositions on (extended) event-orderings, called agreement (all decision events have the same value) and responsiveness (the value decided on must be one of the values proposed): 8e1; e2 : E(D): D(e1) = D(e2) 8e : E(D): 9e0 : E(P ): e0 < e ^ D(e) = P (e0)
It is easy to prove about TwoThirds the safety property that if there are two decide events, say Decide(e) and Decide(e0), then Decide(e) = Decide(e0). We can also show that if Decide(e1) = v, then there is a prior input event, e0 such that Input(e0) = Decide(e1).
We can prove safety and the following liveness property about TwoThirds. We say that activity in the protocol contracts to a subset S of exactly 2f + 1 processes if these processes all vote in election n say at vt(n)1; :::; vt(n)k for k = 2f +1 and collect these votes at c(n)1; :::; c(n)k, and all vote again in election n+1 at vt(n+1)1; :::; vt(n+1)k, and collect at c(n+1)1; :::; c(n+1)k. In this case, these processes in S all decide in round n + 1 for the value given by f applied to the collected votes. This is a liveness property.
If exactly f processes fail, then the activity of the group G contracts to some S and decides. Likewise if the message tra c is such that f processes are delayed for an election, then the protocol contracts to S and decides. This fact shows that the TwoThirds protocol is nonblocking, i.e. from any state of the protocol, there is a path to a decision. We can construct the path to a decision given a set of f processes that we delay.
We also proved safety and liveness of a variant of this protocol that may converge to consensus faster. In this variant, if Pi receives a vote he; vi from a higher election, e > eli, then Pi joins that election by setting eli := e; vi := v; and then going to step 2. 3.5
Networked systems will be attacked. One way to protect them is to enable them to adapt to attacks. One way to adapt is to change the protocol, but this is dangerous, especially for the most critical protocols. The responsible system administrators don't ever want to modify the most critical protocols such as consensus. One alternative is to switch to another provably equivalent protocol, a task familiar to us from the stack optimization work. So we proposed to formally generate a large number of logically equivalent variants, store them in an attack response library, and switch to one of these variants when an attack is detected or even proactively. Each variant uses distinctly di erent code which a system under attack can install on-the- y to replace compromised components. Each variant is known to be equivalent and correct.
We express threatening features of the environment formally and discriminate among the
di erent types. We can do this in our new GPM model because the environment is an explicit
component about which we can reason. This capability allows us to study in depth how diversity
works to defend systems. We can implement attack scenarios as part of our experimental
platform. It is interesting that we can implement a constructive version [
Synthetic Code Diversity We introduce diversity at all levels of the formal code development (synthesis) process starting at a very high level of abstraction. For example, in the TwoThirds protocol, we can use di erent functions f , alter the means of collecting Msg i, synthesize variants of the protocol, alter the data types, etc. We are able to create multiple provably correct versions of protocols at each level of development, e.g. compiling TwoThirds into Java, Erlang, and F #. The higher the starting point for introducing diversity, the more options we can create.
Acknowledgement The ideas reported here are based on the work of the PRL research group, in particular our research on the logic of events by Mark Bickford, Richard Eaton, and Vincent Rahli, and by our collaboration with David Guaspari of ATC-NY corporation. Our formal work was strongly in uenced by a long term collaboration with Robbert van Renesse and Ken Birman of the Cornell systems group and the recent work of Nicolas Schiper.