Is it possible to write C programs using Coq?

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.

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