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 work proposes to combine 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, while retaining a high guarantee of program correctness and a recognizable connection with the abstract, easily comprehensible semantics.