anchor.diff:            <p>The full definition of the run is then:</p>
             <pre>Definition run_your_name_ok (argv : list LString.t) (name : LString.t)
     : Run.t (your_name argv) tt.
  -  eapply Run.Let.
  -  apply (Run.log_ok (LString.s "What is your name?")).
  -  eapply Run.Let.
  -  apply (Run.read_line_ok name).
  +  eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")).
  +  eapply Run.Let. apply (Run.read_line_ok name).
     apply (Run.log_ok (_ ++ name ++ _)).
   Defined.</pre>
             <p>This run is the Coq formalization of our use case for the valid executions of the computation <code>your_name</code>.</p>
             <p>As another example, here is the formalization of the use case in which the <code>System.read_line</code> command fails (because of a terminal error for instance):</p>
             <pre>Definition run_your_name_error (argv : list LString.t)
     : Run.t (your_name argv) tt.
  -  eapply Run.Let.
  -  apply (Run.log_ok (LString.s "What is your name?")).
  -  eapply Run.Let.
  -  apply Run.read_line_error.
  +  eapply Run.Let. apply (Run.log_ok (LString.s "What is your name?")).
  +  eapply Run.Let. apply Run.read_line_error.
     apply Run.Ret.
   Defined.</pre>
   
  
positive.code: 
            <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 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 its external world.</p>
  
            <h3>Use cases</h3>
            <p>Let us take the previous example of <code>your_name</code>:</p>
  
negative.code:           <p>Once a use case has been formalized, we would like to formally verify it. There is actually... nothing to do, because we know that our runs must be valid since they are well-typed. If we have tried to define an invalid run like:</p>
            <pre>Definition run_your_name_ok (argv : list LString.t) (name : LString.t)
    : Run.t (your_name argv) tt.
    eapply Run.Let. apply (Run.log_ok (LString.s "What is your name? blabla#@!"))
    eapply Run.Let. apply (Run.read_line_ok name).
    apply (Run.log_ok (_ ++ name ++ _)).
  Defined.</pre>
            <p>we would have gotten an error at definition time:</p>
  