--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C native:coq



Hello Loïc,

> Sorry, actually it is not completely clear. The point is that you may can use WP drivers to enrich your proof context with additional theories.
> In these additional theories, you may specify lemmas that can be proved interactively with Why3, or in Coq, or with any another prover.

Thank you for the explanation.

> 
> We are also working with ACSL and WP extensions for a better integration with Why3 and Coq proof support. But I’m afraid it will not be available for the very next release.

Does this mean that the native Coq interface remains in place until these newer development will have been released?
(I would humbly suggest so!-)

Jens