anchor.diff:            <p>In order to be executed, the computations are compiled into OCaml programs with IO. This compilation is done by customizing the <a href="https://coq.inria.fr/refman/Reference-Manual025.html">extraction mechanism</a> used to compile pure Coq expressions to pure OCaml programs. The effects and computation primitives are extracted to explicit <a href="http://ocsigen.org/lwt/">Lwt</a> constructs. Lwt is a popular library for asynchronous IO in OCaml. This compilation phase is not formally verified.</p>
   
             <h2>Verification by use cases</h2>
  -          <p>A popular technique to specify interactive programs with a lot of IO is do define <a href="https://en.wikipedia.org/wiki/Use_case">use cases</a>. A use case is basically a scenario of execution of the program, defined as a list of interaction steps between the program and the external world.</p>
  -
  -          <h3>Use case</h3>
  +          <p>How to exploit the Coq system to verify our programs?</p>
  +          <p>A popular technique to specify interactive programs with a lot of IO is do define a set of <a href="https://en.wikipedia.org/wiki/Use_case">use cases</a>. Basically, a use case is a scenario of execution of the program, defined as a list of interaction steps between the program and the external world.</p>
  +
  +          <h3>Use cases</h3>
             <p>Let us take the previous example of <code>your_name</code>:</p>
             <pre>(** Ask for the user name and answer hello. *)
   Definition your_name (argv : list LString.t) : C.t System.effect unit :=
  
positive.code:           <h2>The effects system</h2>
            <p>What is the definition of a computation with IO and how does this work?</p>
  
            <h3>Effect</h3>
            <p>An effect describes a set of IO or impure operations. An effect is declared by an element of type <code>Effect.t</code>:</p>
            <pre>Module Effect.
    Record t := New {
  
negative.code:           </ul>
            <p>This use case is parametrized by a string <em>name</em>. We could write a test program interacting with <code>your_name</code>, answering the <em>name</em> string to the <code>read_line</code> request and checking that the program outputs are as expected. The limitation of this method is that we can only test a finite number of <em>name</em> values, instead of all the possible strings.</p>
  
            <h3>Runs</h3>
            <p>To cover all the use case instances, Coq.io introduces the notion of <em>run</em>. A run describes one execution of a computation, by programming the behavior of the computation's environment in a particular execution. Said otherwise, a run contains two programs: the computation itself and its environment, with typing rules ensuring that the environment answers to each request of the computation.</p>
            <p>A run is of type <code>Run.t e v</code>, where <code>e</code> is a computation and <code>v</code> is the expected result of the computation. We formally define this type by:</p>
            <pre>Module Run.
  