Is it possible to write C programs using Coq?

Question

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

I present a library that models the C language. Perhaps such a library will contain a set of axioms on how C-constructs interact with process memory, as well as axioms and theorems on IEEE floating-point numbers. Then he will be able to build program C in Coq along with program theorems.

I would use such a library, say, to create a C quicksort algorithm that works with arrays of floats that GCC will compile.

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 proven C software: Verified Software Toolchain , for example, allows us to translate C programs into a format that Coq understands and proves theorems about its behavior. Please note that this evidence has a different taste than you could use if you had done any evidence about Coq programs, because C program simply converts to its syntax tree as Coq data type instead of Coq function.