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 \BSlib{} library, with little to
no loss of performance, while retaining a high guarantee of program
correctness.