The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

On interfacing external theorem provers with Coq in a safer manner, there is recent work like this one: with http://hal.inria.fr/docs/00/63/91/30/PDF/cpp11.pdf

On 3 April 2013 10:16, Jonathan Heras <jonathan.heras AT unirioja.es> wrote:

On 03/04/13 08:58, Claude Marche wrote:

Nevertheless, one should be aware of an important point: when the external prover answers that the goal is valid, then the Why3 tactic introduces an axiom in Coq to discharge the original goal. There is no Coq proof generated. This is an important issue if you want to restrict your trusted code base to the Coq kernel only. As far as I understand, this is not a issue in Isabelle/sledgehammer since Isabelle does not build proof terms internally (am I wrong ?)

In Isabelle, when the external prover answers that a goal is valid, it also returns the lemmas which have been used for that proof. Then, those lemmas are given as input to a program called Metis that tries to reproduce the proof in Isabelle. In some cases, Metis cannot generate the proof even if external prover says that a goal is valid; in those cases, the goal is not admitted and in this way you always work with trusted code.

Cheers,
Jonathan