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.