LOPSTR 2016 Invited Talk
Challenges in Compiling Coq
Abstract. The Coq proof assistant is increasingly used for constructing verified
software, including everything from verified micro-kernels to verified
databases. Programmers typically write code in Gallina (the core
functional language of Coq) and construct proofs about those Gallina
programs. Then, through a process of "extraction", the Gallina code
is translated to either OCaml, Haskell, or Scheme and compiled by a
conventional compiler to produce machine code. Unfortunately, this
translation often results in inefficient code, and it fails to take
advantage of the dependent types and proofs. Furthermore, it's a bit
embarrassing that the process is not formally verified.
Working with Andrew Appel's group at Princeton, we are trying to
formalize as much of the process of extraction and compilation as we
can, all within Coq. I will talk about both the opportunities this
presents, as well as some of the key challenges, including the
inability to preserve types through compilation, and the difficulty
that axioms present.