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

[Frama-c-discuss] Using Coq as prover



Hi Jens,

> As far as I understand it, the interaction of WP with Coq will move away from the native:coq interface
> to the Why3 interface.
> It might well be that with respect to the coq scripts the changes might not be so severe.
> In other words, just start working with native:coq and hope for the best!

that sounds like good advice!

Best regards
Matthias