Re: Beside of SPARK: how do you compare Alt-Ergo and Coq?

[Phil Clayton <phil.clayton@lineone.net>]

On Feb 21, 3:24 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> If I'm wrong with this question here, just tell me. Many people here have
> a lot of interest in such topics, and I though this may be another (again)
> opportunity to link both to Ada. At least AdaCore already did with
> Alt-Ergo which can be used as a prover in conjunction with SPARK. I know
> the Alt-Ergo system was proved with Coq. Both Alt-Ergo and Coq are prover
> or proof checker, but how do you compare both?

I've not used either so can only add some general comments.  The most
apparent difference is that Alt-Ergo is an automatic theorem prover
whereas Coq is an interactive theorem prover, with automatic proof
support.  An interactive theorem prover allow every step of the proof
to be controlled whereas an automatic prover typically uses a
predefined proof strategy that users have only a high-level of control
over, e.g. by adding rules, setting options etc.  In principle, the
programmable nature of interactive theorem provers allows any
automatic proof procedure to be implemented but the 'burden' of
ensuring logical consistency in any proof introduces overheads that
may not be worthwhile for some people.

I would recommend starting with an interactive theorem prover (like
Coq) to get an understanding of the concepts involved in theorem
proving.


> I know Coq uses
> intuitionistic logic. What about Alt-Ergo? Intuitionistic too?

For program verification, I think you would want to be able to deduce,
for a proposition P, things like "P or (not P)" (excluded middle) and
"not (not P) = P", which intuitionistic logic can't on its own.
Sacrificing constructiveness of the logic by adding these facts
wouldn't be an issue for verification.  Furthermore, the
intuitionistic logic can probably embed a logic with these facts (I am
a bit hazy here).  However from what I have read about Alt-Ergo it
looks like it is generic, in the sense that the theory is determined
by the particular equational theories supplied by a user.  (Can
someone confirm this?)

For Coq, logic consistency is dependent on only a very small amount of
fixed code as it is built in the LCF-style.  My guess is that the
consistency of proofs with Alt-Ergo is dependent on the consistency of
the equational theories supplied by users.  (I would be interested to
know for certain.)


> Alt-Ergo is already used with SPARK/Ada. Coq too? These are the main
> questions I have in mind.

I hear that Microsoft's Z3 was also used on SPARK VCs with good
results.  I don't know about Coq.

Another difference between interactive and automatic theorem provers
you may like to consider: what do you do when an automatic prover does
not complete a proof?

Phil