Using Coq to Write Fast and Correct Haskell

John Wiegley and Benjamin Delaware

abstract

Correctness and performance are often at odds in the field of systems engineering, either because correct programs are too costly to write or impractical to execute, or because well-performing code involves so many tricks of the trade that formal analysis is unable to isolate the main properties of the algorithm.

As a prime example of this tension, Coq is an established proof environment that allows writing correct, dependently-typed code, but it has been criticized for exorbitant development times or forcing the developer to decide between optimal code or tractable proofs. On the other side of the divide, Haskell has proven to be a capable, well-typed programming environment, but easy-to-read, straightforward code must all too often be replaced by highly optimized variants that obscure the author's original intention.

This work proposes combining these two environments: allowing declaratively stated, proof-amenable specifications to be developed in Coq at a high level of abstraction, while still permitting correct-by-construction implementations that meet or exceed the performance demands of highly optimized Haskell. As a case study, we reimplement a subset of the popular ByteString library, without any loss of performance, but with a high guarantee of program correctness, and a recognizable connection with the abstract, easily comprehensible semantics.