Doug Howe - Combining functional programming languages and set theory in support of software verification

Computer systems for proving theorems can be coarsely classified as either automatic or interactive. Automatic systems require theorems to be stated in a simple formalism, such as equational logic or ordinary first-order logic, and use a proof-search procedure that requires little or no guidance from the user. While such systems have produced impressive results in certain branches of mathematics, their proof-search procedures become overwhelmed when proofs require a substantial amount of background knowledge, for example when the provers are used for verifying correctness properties of software (and hardware) systems. Virtually all successful applications of theorem provers to verification problems have used interactive systems, where a human user is relied upon to provide the main ideas for the proof, and the system handles the trivial details.

Because of the central role of the user in interactive systems, there has been a great deal of research into formalisms that allow users to express their problems and proof ideas as directly and concisely as possible. Some of the formalisms currently in use are constructive. These logics are designed to allow direct expression of concepts from programming and to get at the computational content of mathematics. Other formalisms are classical, and are used to give conventional mathematical models of software and hardware systems. In this talk, we describe our attempt to unify the two kinds of formalisms. The goal is a logic that supports direct reasoning about programs and abstractions related to programming, and at the same time has the mathematical modelling power of set theory ( ZFC). The technical core of our work is a way to combine functional programming languages with conventional concepts from set theory.