The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-11-24 19:32 GMT+01:00 Frédéric Besson <frederic.besson AT inria.fr>:

Hello,

Do not worry for my soul, I won’t be doomed : I fear no evil.
Being pragmatic is a shortcut not a shortcoming!

I am familiar with monads — turning an existing code in monadic style for the only purpose of tracing/logging  would be a waste of time.

The proposal of matej makes sense but I feel that some axiomatisation of the Trace function would be necessary.

I was proposed other solutions from teammates:
In the Verasco project, they add a fake dependancy and limit inlining.
It is also possible to patch the extraction of a « tracer » function— with some notations it looks non intrusive.

BTW, I am curious about what could really go wrong ?
What kind of Coq property can be broken — by an axiom of the form :

Axiom IAmAnyTypeSafeOCamlProgram : A -> unit with the additional assumption that A is a ML type.

​Such an axiom has no problem on the Coq side. After all, there is a function which does this in Coq (fun _ => tt)​, and the problems you can encounter when implementing it are not bound to the unit type. With Ocaml, as soon as you have a _ -> _ some side effect can occur.

 

I see that this code could raise an exception or abort the Coq program — does not sound so bad.
If A is polymorphic and is used in OCaml with some mutable data-structure, anything could happen — this sounds bad.

Other scenarios ?

​You do not need A polymorphic, you could also have A as an Àxiom A : Type. Which would then be implemented by a type with mutable fields.

​You could also have A=unit, with a side effect on a global mutable variable, which would break things.

For instance in Ocaml, you could have a "get_counter : unit -> int", "inc_counter : unit -> unit" and some extracted code using these functions.

"inc_counter" could seem completely harmless, but it could in fact hide something more harmful.

 

Thanks,
—
Frédéric





> On 23 Nov 2015, at 17:43, Cedric Auger <sedrikov AT gmail.com> wrote:
>
> ​There is no side effect in Coq, assuming extraction will manage side effects is wrong.
> (Think of extraction to Haskell which has no side effect, unless you do really dirty things.)
> If your real code uses side effect, then you loose most of the point of having done your proofs in Coq.
> Still, you are not doomed, as you can rely on some tricks, like monads (if you do not know anything about monads, you should probably read a little about them, it could be useful to solve your problem).
>
> Declare a constant of type "state -> nat -> state", and pass sequentially all your states to your functions.
> Then implement "state" with what ever you want.
>
> Parameter state : Type.
> Definition sequence := state -> state.
>
> Parameter trace_nat : nat -> sequence.
>
> (* print all nats from n to 0 *)
> Definition count_down​ : nat -> sequence :=
>   fix count_down (n : nat) : sequence :=
>   match n with
>   | O => trace_nat O
>   | S n => fun s =>
>            let s := trace_nat (S n) in
>            count_down n s
>   end.
>
> ​And then for you extracted code, you can do a side effect with implementing "state" with "unit",
> and "trace_nat : nat -> unit -> unit" (ok there is one "unit" more) as "fun n () => print_nat n".
> Of course, your "main" function will have an extra "unit" parameter.
>
> That should solve your problem, as with that, the state must be kept and follow some path from "inputs" to "outputs".
> Being abstract, the extraction cannot optimize anything on it, and must be keep the result.
> This also ensure sequential execution of all your "side effect" stuff.
>
> You can even simply not implement "state" with a side effect, but with a list of natural numbers.
> Then you could run your "main" program with the empty list, and then print the whole list as result (but storing the list might take a lot of space).
>
>
>
>