anchor.diff:            <p>The full documentation of the <code>coq:io:system</code> library is available on <em>TODO</em>.</p>
   
             <h3>Your name</h3>
  -          <p>The following program reads a name on the command line and answers hello to this name:</p>
  +          <p>The following program reads a name on the command-line and answers hello to this name:</p>
             <pre>(** Ask for the user name and answer hello. *)
   Definition your_name (argv : list LString.t) : C.t System.effect unit :=
     do! System.log (LString.s "What is your name?") in
  
positive.code: Task of 2 seconds ended.</pre>
  
            <h2>The effects system</h2>
  
            <h2>Verification by use cases</h2>
          </div>
  
negative.code: (** The classic Hello World program. *)
  Definition hello_world (argv : list LString.t) : C.t System.effect unit :=
    System.log (LString.s "Hello world!").</pre>
            <p>We load some libraries and write the <code>hello_world</code> program by calling the <code>System.log</code> function to print a message on the terminal. The return type of the program is <code>C.t System.effects unit</code>, which means this is an <em>impure</em> computation with <em>system</em> effects and returning a value of type <code>unit</code>. The impure computations are the computations which are not purely functional, in the sense they do some IO or modify a state variable for example. The command-line arguments are given by the list of strings <code>argv</code>, but not used here.</p>
  
            <p>To compile the <code>hello_world</code> program, add the lines:</p>
            <pre>Definition main := Extraction.launch hello_world.
  