Coq proof usage

Question

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.

Answer 1

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.