Using Coq to write fast and correct Haskell

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, forcing the developer to choose between optimal code or tractable proofs. On the other side of the divide, Haskell has proven itself to be a capable, well-typed programming environment, yet easy-to-read, straightforward code must all too often be replaced by highly optimized variants that obscure the author's original intention. This paper builds on the existing Fiat refinement framework to bridge this divide, demonstrating how to derive a correct-by-construction implementation that meets (or exceeds) the performance characteristics of highly optimized Haskell, starting from a high-level Coq specification. To achieve this goal, we extend Fiat with a stateful notion of refinement of abstract data types and add support for extracting stateful code via a free monad equipped with an algebra of heap-manipulating operations. As a case study, we reimplement a subset of the popular bytestring library, with little to no loss of performance, while retaining a high guarantee of program correctness.