We present an original approach to sound program
extraction in a proof assistant, using
syntax-driven automation to derive
correct-by-construction imperative programs from
nondeterministic functional source code. Our
approach does not require committing to a single
inflexible compilation strategy and instead
makes it straightforward to create
domain-specific code translators. In addition
to a small set of core definitions, our
framework is a large, user-extensible collection
of compilation rules each phrased to handle
specific language constructs, code patterns, or
data manipulations. By mixing and matching
these pieces of logic, users can easily tailor
extraction to their own domains and programs,
getting maximum performance and ensuring
correctness of the resulting assembly code.
Using this approach, we complete the first
proof-generating pipeline that goes
automatically from high-level specifications to
assembly code. In our main case study, the
original specifications are phrased to resemble
SQL-style queries, while the final assembly code
does manual memory management, calls out to
foreign data structures and functions, and is
suitable to deploy on resource-constrained
platforms. The pipeline runs entirely within
the Coq proof assistant, leading to final,
linked assembly code with overall
full-functional-correctness proofs in separation
logic.