[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Comparison between TLAPS and other proof assitants


Spin stands apart from the other systems that you mention in that it is a model checker whose language is deliberately restricted so that verification becomes efficient. In fact, Spin translates a Promela model into a C program that contains a model checker that is specific to that particular model.

Concerning proof assistants such as Agda, Coq, HOL, Isabelle, NuPRL, PVS etc., they differ according to their logical foundations (and you'll find strong opinions in the various sub-communities on why some logic is more appropriate than another one), but for all practical purposes I personally do not think that differences in expressiveness are relevant. You will be able to express any system specification, correctness property, and proof, or even your favorite mathematical theory, in any of these systems. Of course, each system may have its idiosyncrasies and you may feel more or less comfortable with how the concepts you are interested in are expressed. After all, the most powerful system is of no use to you if you feel that you constantly need to work against your intuitions for expressing them in the language of the system. For advanced use, the existence of a standard library of theories (definitions and proofs) relevant for your formalization will become a decisive factor. Other dimensions are the degree of proof automation, maturity of the system, trustworthiness of the kernel, IDE support etc.

A somewhat dated, but still relevant comparison was published as an LNCS volume by Freek Wiedijk in 2007 [1] and is worth reading.


[1] http://www.cs.ru.nl/~freek/comparison/, see also https://dblp.uni-trier.de/db/conf/tphol/lncs3600.html and http://www.cs.ru.nl/~freek/comparison/comparison.pdf.

On 5 Feb 2019, at 14:38, Roberto <hous...@xxxxxxxxx> wrote:

Hi All,

I am interested to know how TLA+/TLAPS compares to other proof assistants such as Coq, Isabelle, Spin (an others) especially in term of expressiveness power.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.