From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,58ae2be75e131d99 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Received: by 10.204.153.5 with SMTP id i5mr255598bkw.1.1330024108013; Thu, 23 Feb 2012 11:08:28 -0800 (PST) Path: t13ni61849bkb.0!nntp.google.com!news2.google.com!postnews.google.com!cj6g2000vbb.googlegroups.com!not-for-mail From: Phil Clayton Newsgroups: comp.lang.ada Subject: Re: Beside of SPARK: how do you compare Alt-Ergo and Coq? Date: Thu, 23 Feb 2012 11:08:27 -0800 (PST) Organization: http://groups.google.com Message-ID: References: NNTP-Posting-Host: 94.116.29.22 Mime-Version: 1.0 X-Trace: posting.google.com 1330024107 9511 127.0.0.1 (23 Feb 2012 19:08:27 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Thu, 23 Feb 2012 19:08:27 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: cj6g2000vbb.googlegroups.com; posting-host=94.116.29.22; posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe User-Agent: G2/1.0 X-Google-Web-Client: true X-Google-Header-Order: HUALENKRC X-HTTP-UserAgent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0) Gecko/20100101 Firefox/10.0,gzip(gfe) Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Date: 2012-02-23T11:08:27-08:00 List-Id: On Feb 21, 3:24=A0am, Yannick Duch=EAne (Hibou57) 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) =3D 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