anchor.diff:            <pre>Task of 4 seconds ended.
   Task of 2 seconds ended.</pre>
   
  -          <h2>The effects system</h2>
  +          <h2 id="effects">The effects system</h2>
             <p>What is the definition of a computation with IO and how does this work?</p>
   
             <h3>Effects</h3>
  
positive.code:   end.</pre>
            <p>We use the function <code>System.eval</code> to evaluate a command and get its status code and output. If the two <code>uname</code> calls are successful, we retrieve the OS and machine names and display them. The <code>0%Z</code> stands for the zero in the type <code>Z</code> of the relative integers. A null value means by convention that the commands were successful.</p>
  
            <h2>Use concurrency</h2>
            <p>In order not to freeze, interactive programs usually need to run many IO operations in parallel. Consider for example an application which must keep a reactive user interface while doing slow network operations.</p>
            <p>To run two operations in parallel, we use the <code>join</code> operator:</p>
            <pre>join : C.t E A -> C.t E B -> C.t E (A * B)</pre>
  
negative.code:           <h3>Compilation</h3>
            <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 id="use-cases">Verification by use cases</h2>
            <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 to 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 its external world.</p>
  
  