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

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

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