3

I'm a beginner with Coq, I learnt the language quickly, to do proofs etc.

But I don't understand what can we do with this. Ok we prove some definitions etc. But in which ways can we use them? I saw that we can extract in Haskell files, but I don't understand it either.

Because I would like to use the language to prove CVE for example.

Improve this question

1 Answer 1

Reset to default
6

One of the uses of Coq is verifying software. This means writing down a program and showing that it satisfies some specification that you care about. What counts as a specification is rather open ended: you might want to show that a C program does not suffer from buffer overflows, or that a compiler produces object code that behaves according to the specification of the source language.

There are two main ways of verifying software in Coq.

Internal verification

One possibility is to implement the program as a functional program that can be executed inside of Coq, and prove properties about it. This program can be extracted to a more conventional programming language such as Haskell or OCaml. You can then link this code against other modules in the extraction target to produce a complete executable. This is the approach, for instance, followed by the CompCert C compiler.

For concreteness, suppose that we want to write a verified sorting algorithm. Here is an implementation of insertion sort in Coq that uses the Mathematical Components library:

From Coq Require Import Extraction.
From mathcomp Require Import all_ssreflect.

Fixpoint insert n ns :=
  if ns is m :: ns then
    if n <= m then n :: m :: ns
    else m :: insert n ns
  else [:: n].

Lemma sorted_insert n ns : sorted leq ns -> sorted leq (insert n ns).
Proof.
case: ns => //= m ns m_ns; rewrite fun_if /=.
case: ltngtP => // /ltnW m_n.
elim: ns => [|p ns IH] /= in m m_ns m_n *; first by rewrite m_n.
case/andP: m_ns => m_p m_ns; rewrite fun_if /= m_n m_p.
by case: ltngtP => //= /ltnW p_n; rewrite IH.
Qed.

Fixpoint insertion_sort ns :=
  if ns is n :: ns then insert n (insertion_sort ns)
  else [::].

Lemma sorted_insertion_sort ns : sorted leq (insertion_sort ns).
Proof.
by elim: ns => //= n ns IH; rewrite sorted_insert.
Qed.

Extraction "insertion.ml" insertion_sort.

If you compile this file, you will see that it will generate an insertion.ml file that contains a translation of this program in OCaml.

External verification

Another possibility is to give a mathematical description of the behavior of your program and prove that this description is correct. For example, we can use Coq to define the behavior of C programs as a mathematical relation between inputs and outputs, and then use this description to argue that a particular C program is correct (i.e., that its sequence of inputs and outputs satisfy some property). This particular C program might be translated from actual C source code into a form that Coq understands, as done by the Verified Software Toolchain.

What does this mean?

A Coq proof guarantees that certain bugs cannot arise in an idealized model of program execution. Regardless of which verification approach you chose, this model is much simpler than what happens when a program actually runs. For instance, we don't bother modelling the laws of physics that describe the circuits of the processor that is running the program, because that would be too complex. However, most bugs that we care about can be described in terms of fairly simple models -- for example, we don't need detailed laws of physics to explain why a buffer overflow occurs in some execution. This makes Coq and related tools very effective at preventing bugs in practice.

Improve this answer
4
  • I understand much better now, thank you very much! One last thing, I understood the main ideas that you said. But I still don't get, at the end, how can we check that the C program does not suffer from buffer overflows, or behaves properly? Is it possible to give me a short example (an addition or whatever) from step one to last step, to show me how can I verify that the C program is working properly? And for example, what can I do with the insertion.ml in your Internal verification example?
    – ARevX
    Commented Mar 17, 2022 at 15:04
  • It's hard to give a short example of verifying a C program without discussing the infrastructure needed to do so. I suggest you have a look at the first chapter of the Verifiable C book to get a clearer picture: softwarefoundations.cis.upenn.edu/vc-current/…. As for the insertion sort example, you can run this program with the guarantee that it is correct. Running the program by itself is usually not very interesting because Coq cannot do IO, but you can call it from another big program. I suggest you try to download and compile CompCert to see how this works.
    – Arthur Azevedo De Amorim
    Commented Mar 17, 2022 at 17:17
  • Thank you for your answer, but I'm even more lost with this, because from my point of view it's look so hard to deal with a Coq proof. Do you have any examples, any documentations, that could help me to understand better how a Coq proof can be useful, in an easy way? Not necessarily verifying software. In my case, what I would like to do, is representing the behavior of something, defining properties, lemmas, axioms, etc, and to use them. For example representing the behavior of a stack, either interacting with it, or proving that it's working well. Thank you again.
    – ARevX
    Commented Mar 18, 2022 at 8:31
  • I am not sure what you mean by "useful", but if you are trying to understand how to model systems, I am afraid to need to work through an entire book like Software Foundations (softwarefoundations.cis.upenn.edu) to get the hang of it. It is not something that can be summarized well in a SO answer. (Here is a short example describing the implementation of a stack, since you mentioned it: github.com/kisom/okasaki-coq/blob/master/stack.v.)
    – Arthur Azevedo De Amorim
    Commented Mar 18, 2022 at 11:53

Not the answer you're looking for? Browse other questions tagged or ask your own question.