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.

score 10 · Accepted Answer · answered Oct 23 '17 at 21:43

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.

The book edited by Andrew Appel is a bit out of date with the current VST, but it's a good introduction to the ideas. — Benjamin Pierce, Oct 25 '17 at 10:30

score 3 · Answer 2 · answered Dec 31 '20 at 21:30

3

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

answered Dec 31 '20 at 21:30

Mark

5,286
5
42
73

Is it possible to write C programs using Coq?

2 Answers2