Two main properties make type systems an effective and scalable formal method. First, important classes of programming errors are eliminated by statically enforcing the correct use of values. Second, types facilitate modular software development by serving as specifications of program components, while hiding the component’s actual implementation. Implementations with the same type can be interchanged, thus facilitating software reuse and evolution.

Mainstream type systems focus on specifying relatively simple properties that admit type inference and checking with little or no input from the programmer. Unfortunately, this leaves a number of properties, including data structure invariants and API protocols outside of their reach, and also restricts the practical programming features that can be safely supported. For example, most simply-typed languages cannot safely allow low-level operations such as pointer arithmetic or explicit memory management.

In this talk, I will describe Hoare Type Theory (HTT) which combined dependent types of a system like Coq with features for specification and verification of low-level stateful operations in the style of Hoare Logic.

Such a combination is desirable for several reasons. On the type-theoretic side, it makes it possible to integrate stateful behaviour into dependent type theories that have so far been purely functional. On the Hoare Logic side, it makes is possible to use the higher-order data abstraction and information hiding mechanisms of type theory, which are essential for scaling any kind of verification effort. For example, by combining type-theoretic abstractions with Hoare-logic types, we are able to capture the specifications for local higher-order state, as well as encode the main ideas from Separation Logic.

From the technical standpoint, it is interesting that the design of HTT relates in an essential way some of the most venerable ideas from programming language theory such as Dijkstra’s predicate transformers, Curry-Howard isomorphism and monads. I will discuss the implementation of HTT, verification of various examples that I have carried out, as well as the possibilities for scaling HTT to support further programming features, such as concurrency.