anchor.diff:  ./main.native</pre>
             <p>This should display <code>Hello world!</code> on the terminal.</p>
   
  -          <h2>More examples</h2>
  +          <h2 id="examples">More examples</h2>
             <p>The full documentation of the <a href="https://github.com/coq-io/system"><code>coq:io:system</code></a> library is available on <a href="http://coq-io.github.io/doc/system/2.3.0/toc.html">v2.3.0</a>.</p>
   
             <h3>Your name</h3>
  
positive.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>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>
  
  
negative.code:           <pre>Task of 4 seconds ended.
  Task of 2 seconds ended.</pre>
  
            <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>
  