Is it possible to write C programs using Coq?

Question

I know that one can extract Coq programs into Haskell and OCaml programs. Is there a way to do this with C?

I am imagining a library that models the C language. Maybe such a library would contain a collection of axioms about how C constructs interact with process memory, and axioms and theorems about IEEE floating point numbers. Then it would be able to build a C program within Coq along with theorems about the program.

I would use such a library, say, to build a C quicksort algorithm that works on arrays of floats that would be compilable by GCC.

Answer 1

C is not available as an extraction target for Coq programs; only OCaml and Haskell are supported. However, we can still use Coq to write verified C software: the Verified Software Toolchain, for example, allows us to translate C programs to a format that Coq understands and prove theorems about their behavior. Note that these proofs have a different flavor than you might be used to if you have done any proofs about Coq programs, because the C program is simply converted to its syntax tree as a Coq data type, instead of a Coq function.

Answer 2

There is a new Software Foundations chapter that deals with the practicals of interfacing Coq and C.