The Ynot Project: Overview

Background and Motivation

Dependent type theories, such as the Calculus of Inductive Constructions (as implemented in the Coq proof assistant) provide a powerful, uniform way to write (a) functional programs, (b) specifications and models that capture desired properties of programs ranging from simple typing and safety properties up to full correctness, and (c) formal, machine-checked proofs and tactics that a given program meets its specification. For example, Xavier Leroy and his students have used Coq to construct an optimizing compiler that translates a (well-defined) subset of C to PowerPC code, defined operational semantics for both C and PowerPC code, and mechanically proved that when the compiler succeeds in producing target code, that code behaves the same as the source code, thereby establishing the correctness of the compiler. Coq is not alone in providing support for this style of program development: Other examples include ACL2, Isabelle, NuPRL and MetaPRL, and Epigram.

Nevertheless, today's dependent programming environments suffer from a number of limitations that limit their applicability. One serious shortcoming, and the shortcoming on which Ynot is focused, is that we are limited to writing and reasoning about only purely functional programs with absolutely no side effects, including recursion, mutable state, exceptions, I/O, concurrency, etc. While some programming tasks, such as a compiler, can be formulated as a pure, terminating function, most important tasks cannot. Furthermore, even "functional" programs such as a compiler need to use asymptotically efficient algorithms and data structures (e.g., hash-tables) but current dependently typed languages prevent us from doing so.

Why We Found Alternative Approaches Insufficient

An alternative to starting with a dependent type theory is to start with a standard effectful programming language, such as Java, C#, Haskell or ML, and attempt to retrofit facilities for expressing models, specifications, dependency, refinement, and proofs. For example, the JML and Spec# projects extend Java and C# respectively with support for Hoare-style pre- and post-conditions as well as object invariants and other features needed to capture safety and correctness requirements of code. For Spec# (and the ESC-Java system which is based on a subset of JML), an automated SMT-style prover is used to try to discharge proof obligations and establish that the code meets its specification.

While there have been great advances in automated prover technology over the past few years, these systems still have trouble discharging all but the most "shallow" specifications. In particular, they are extremely useful for weeding out low-level coding problems (such as an array index out of bounds or a NULL-pointer dereference), but their capabilities fall well short of something like Leroy's certified compiler. In contrast, dependent type theories make it possible to utilize automated deduction techniques, but when they fall short, also allow the programmer to construct explicit proofs of "deep" properties of programs. For programs where deep reasoning matters, we must acknowledge that programmers will play an integral role in co-developing models, specifications, programs, and proofs.

Furthermore, the modeling and specification languages used by JML and Spec# are too weak to support a truly modular development of programs and specifications. As a simple example, neither language has the expressive power to capture a principal specification for "compose" or "map" or any other higher-order combinator. And while each language provides impressive mechanisms for helping to modularize the reasoning about some common classes of effectful computations (e.g., through modifies clauses, ownership types, object invariants, etc.), these mechanisms end up being simultaneously complicated and yet frustratingly incomplete.

There is another emerging class of projects that are attempting to retrofit dependent typing to effectful programming languages based on indexed or phase-split dependent types. Notable examples include Hongwei Xi's DML and more recent ATS, Tim Sheard's Omega, and Walid Taha's Concoqtion. These systems have a strong separation between the programming language (which includes effects) and the specification languages (which do not.) For example, in Concoqtion, the programming language is based on OCaml, but the specification language is based on Coq. Coq terms can be used to index ML type constructors that classify values, so it becomes possible, for instance, to use the types to capture correctness requirements. The systems have re-discovered the power of inductive definitions through the use of so-called generalized abstract data types (GADTs) which have long been present in Coq, but only recently reflected (in a limited fashion) into languages such as Haskell and OCaml.

While indexed types and GADTs are one way to solve the inherent problems needed to ensure soundness of a dependency in the pressence of effects, they have many shortcomings in the current realizations. First, neither ATS, Omega, nor Concoqtion can use indexed types to suitably capture and reason about effects themselves (e.g., updates to a mutable store.) Thus, while programmers can write effectful code, they can only reason completely about the pure subset, and cannot capture specifications or requirements on effects. Second, the awkward split between models, specifications, and code means that many definitions must be duplicated leading to a verbose style that is difficult to write and maintain. For example, to fully capture the behavior of a function that appends two lists, we must, in essence, code the append operation at both the specification level and the program level and link them through the use of singleton types.

Yet another approach for incorporating dependency and refinement is typified by the Sage and Deputy projects and more generally with "design-by-contract" languages such as Eiffel and the excellent work in PLT Scheme. Here, programmers write boolean expressions as pre- and post-conditions that are intended to be executed at run-time. In Sage and Deputy, an analysis is used to try to optimize away contracts, or to show that the contracts will fail at run-time. A key advantage of these systems is that programmers need not learn a new specification language and programmers can take advantage of existing code within their specifications. Furthermore, by restricting the specifications to boolean functions, we can always fall back on run-time tests when a theorem prover is unable to discharge the requirement at compile time.

In practice, however, these systems have a number of problems: Of course, one problem is the potential overhead of running the contracts and thus programmers who worry about performance will tend to only use simple "local" contracts. Another problem is that, especially in the presence of concurrency, one must be careful about race conditions, deadlocks, etc. when the contracts examine shared state. Finally, they key issue is that the boolean functions used as contracts must only contain "benign" effects in order to safely optimize them away without changing the behavior of the program. If we enforce that the boolean functions must be "pure" according to some syntactic or typing criteria, then in practice, we cannot always use existing or efficient code for the contract. As a simple example, consider a splay-tree lookup which happens to re-balance the tree: The effects are benign (because eliminating the lookup is safe) but demands a deep proof. If on the other hand, we don't enforce purity, then the "meaning" of the contract is suspect and we lack coherence.

In practice, all of these approaches are good practical steps towards realizing more advanced programming environments with some support for dependent types and in practice, we believe that a combination of these ideas, built on a more general framework, will provide better solutions.

Our Approach: Hoare Type Theory

The approach we are taking is to extend Coq, which already has good support for functional programming, inductive definitions, specifications, proofs, and tactics by adding a new type constructor known as the Hoare Type, and written as ST p a q. Intuitively, the type constructor ST classifies delayed, possibly effectful computations, much the way that the IO-monad is used to separate effectful computations in Haskell. Unlike Haskell, our monad is indexed not only by the return type of the computation, but also a pre-condition and post-condition. Intuitively, when a computation of type ST p a q is run in a world w₁ satisfying the pre-condition p, then if the command terminates, it will produce a value x of type a and result in a new world w₂ such that the predicate q x w₁ w₂ holds. Currently, worlds are modeled as heaps that map locations to values. Computations can allocate new locations, read or write the contents of a location (performing strong updates), and even deallocate locations. Computations can also throw and catch exceptions, or diverge.

As a simple example, here is a Ynot definition that increments the contents of a location, and returns the original value:

Definition inc x := v <-- !!x; x ::= (v+1);; ret v.

This definition takes advantage of some syntactic definitions. In particular "x <-- M; N" is short-hand for "bind M (fun x => N)", "M ;; N" is short-hand for "bind M (fun _ => N)", "!!M" is short-hand for "read M", and "M ::= N" is short-hand for "write M N". Thus, when de-sugared, the actual definition is given by:

Definition inc x :=
   bind (read x) (fun v => bind (write x (v+1)) (fun _ => ret v))).

So the basic operations for constructing and composing ST computations consist of the "ret" (return) and "bind" operations for the monad, together with primitive computations such as read and write. Let us examine the types of each of these primitives and see how they fit together. Note that in what follows, we will gloss over exceptions to keep the presentation simple.

The type for return is as follows:

ret : forall (A:Type) (x:A),
         ST (fun w1 => True) A (fun v w1 w2 => v=x /\ w1 = w2)

In English, "ret T M", where "T" is the type of the term "M", yields a computation which can be run in any world (the pre-condition maps worlds to True) and yields a value v which must be equal to M, and a new world equal to the original. The return operation allows us to lift a pure Coq computation into the world of effectful commands. Thus, as an imperative language, Ynot inherits all of Coq for its "pure" subset, and the types are reflecting the distinctions between pure and impure code. Note that in Coq, certain arguments, such the Type argument A, can be automatically inferred so we only need to write "ret M". In the subsequent examples, we will elide the type and predicate arguments as Coq can infer these.

The type for read is as follows:

read : forall (A:Type)(x:loc),
          ST (fun w1 => exists v:A, points_to x v w1)
          A
             (fun v w1 w2 => points_to x v w1 /\ w2 = w1)

Thus "read M" yields a computation which can only be run in a state where M points to some value v of type A, and it produces that value as a result, leaving the state of the world unchanged. The type for write is similar:

write : forall (A:Type)(x:loc)(v:A),
         ST (fun w1 => exists B, exists z:B, points_to x z w1)
            unit
            (fun _ w1 w2 => w2 = update w1 x z)

Therefore, "write M N" yields a computation which can be run in a state where M points to some value and it yields a new state that is equal to the functional update of the original state at location M with the value N of type A. Note that the update is strong in the sense that it doesn't require that we write values of the same type into locations.

Finally, the type for "bind" is the crucial one, as this is what allows us to (sequentially) compose operations:

bind : forall (A B:Type)
                 (p: pre)(q : post A)
                 (r:A->pre)(s:A->post B)
                 (c1 : ST p A q)(c2 : forall x:A, ST (r x) B (s x)),
                   ST (fun w1 => p w1 /\ forall x w, q x w1 w -> r x)
                       B
                      (fun y w1 w2 => exists x w, q x w1 w /\ s x y w w2)

In words, "bind M N", where M has type ST p A q and N has type forall x:A, ST (r x) B (s x) yields a computation where the pre-condition includes p, but also requires that whenever we have an intermediate state satisfying the post-condition of M, then this should imply the pre-condition of N, namely r. This is the weakest pre-condition of the compound command that ensures we can safely run M and then N. The post condition is simply the relational composition of q and s, the two post-conditions of the commands. Again, this is the strongest post-condition that one can formulate. Notice that the definition of bind required that we abstract not only over types and commands, but also predicates in order to ensure we can get the weakest pre-condition and strongest post-condition (i.e., a principle type.) This shows how central predicate abstraction is to composition when we wish to employ Hoare-style reasoning.

Ynot will automatically calculate the weakest pre-condition and strongest post-condition for the command, just as it will infer types. Unfortunately, these specifications are not always readable or what you might expect. For instance, Ynot infers the following type for inc:

forall x : loc,
   ST (bind_pre (read_pre nat x) (read_post nat x)
        (fun v : nat => bind_pre (allocated x) (write_post x (v+1))
        (fun _ : unit => nopre)))
      nat
      (bind_post (read_pre nat x) (read_post nat x)
        (fun v : nat => bind_post (allocated x) (write_post x (v+1))
        (fun _ : unit => ret_post v)))

which uses a number of auxilliary definitions that abstract the pre and post-conditions of the various commands, but even when these are reduced the result is unreadable. We use the "do" primitive to coerce a computation with one specification into a specification that is either equivalent, or implied by the principal specification inferred by Ynot. The type of the "do" primitive is:

do : forall (A:Type)(p r:pre)(q s:post A)
              (pf : forall w1, r w1 ->
                    (p w1 /\ forall x w2, q x w1 w2 -> s x w1 w2)),
          ST p A q -> ST r A s.

So do takes an ST p A q and coerces it to an ST r A s, but we must provide a proof that this coercion is justified. In particular, we must show that r implies p, and q implies s, which corresponds the the usual rule of consequence in Hoare logic. As an example, we can use "do" to ascribe a more readable specification to the inc definition as follows:

Program Definition inc(x:loc) : ST (fun w1 => exists v:nat, points_to x v)
                                     nat
                                    (fun v w1 w2 => points_to x v w1 /\
                                                    w2 = update w2 x v)
   := do _ (v <-- !!x; x ::= (v+1);; ret v).

This specification is a natural one for inc that is logically equivalent to what Ynot infers, but we can also choose to strengthen the pre-condition (e.g., require that x's initial value is greater than zero) or weaken the post-condition. In the example above, we used Coq's Program construct to avoid having to enter the proof obligation that "do" demands. Rather, we've put in a place-holder (the underscore) which allows us to write the definition and type-check it, and then discharge the proof obligation using a proof script and/or tactics. In this particular case, we have a simple tactic (avcsimps) that can automatically discharge the proof obligation. A long term goal for us is to develop more tactics and decision procedures, as well as more refined definitions that make discharging proof obligations simpler.

In practice, the ST monad should not be directly used for programming because it forces you to reason about the entire world (i.e., the whole heap). To address this problem, we have defined an alternative monad, STsep on top of the ST monad which provides a "small footprint" approach to specifying and reasoning about pointer-manipulating programs in the spirit of Separation Logic. However, we do not yet have good tactics for discharging the attendent proof obligations and see this as a major research issue.

Finally, in addition to the ST and STSep monads, we have developed the theory (but not yet the implementation) of a concurrent version of Ynot with support for software-based transactional memory in the style of GHC's STM monad. We hope to release definitions and code soon, but for now, please contact us if you are interested in more details.