The Coq mailing list

[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.

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 ?

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).
> 
> 
> 
>

Attachment: signature.asc
Description: Message signed with OpenPGP using GPGMail