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

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

[Yannick Duchêne (Hibou57)]

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 know Coq uses  
intuitionistic logic. What about Alt-Ergo? Intuitionistic too? Now  
Alt-Ergo is already used with SPARK/Ada. Coq too? These are the main  
questions I have in mind.

Any pointers welcome. I've not used any of these so far, just planning to  
learn one a bit (but not both). I am not necessarily seeking for  
automatically generated Verification Condition from Ada.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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

[Yannick Duchêne (Hibou57)]

Le Tue, 21 Feb 2012 04:24:48 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> Both Alt-Ergo and Coq are prover or proof checker, but how do you  
> compare both?
So far at least, seems there are far fewer documentations for Alt-Ergo  
than for SPARK and Coq. Or did I miss something or some locations?


-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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

[Yannick Duchêne (Hibou57)]

Le Tue, 21 Feb 2012 04:24:48 +0100, Yannick Duchêne (Hibou57)  
<yannick_duchene@yahoo.fr> a écrit:
> how do you compare both?
The main topic is that Coq cannot be easily used with language others than  
SML/OCaml and Haskell, while Alt-Ergo uses comments as annotations in  
source, like SPARK do. But I could not know how exactly SPARK is linked to  
Alt-Ergo, nor I could find any tiny example of Ada source proved with  
Alt-Ergo.

If any one know some tiny practical examples of Ada+Alt‑Ergo, any pointers  
are welcome.

Another question may be: do Alt-Ergo for Ada depends on SPARK or can be  
independent from SPARK?

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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

[Phil Clayton]

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