Comparison between TLAPS and other proof assitants

[Roberto]

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.

Regards,
Roberto

[saksha...@stonybrook.edu]

Using terminology of [1,2], Coq follows procedural, Isabelle follows declarative and TLAPS follows hierarchical (declarative) style of proof writing. I recommend reading [1] which compares procedural and declarative styles, and then obviously [2] to know the story and insights behind TLAPS's hierarchical style and more. Some of my personal points/feelings are (please note that I'm not an expert in Coq or Isabelle or TLAPS):

* Coq (procedural proofs) is very hard on beginners because of the huge vocabulary of procedures (aka tactics), TLAPS is not

* I am not a huge fan of writing 'this(feels, wrong)' as 'this feels wrong'. It feels like my 20 years of math training has been challenged. TLAPS respects that.

* Without comments, a procedural proof to me is as readable as Mandarin. For example, length_corr in here. TLAPS proofs on the other hand are easily readable because at each step it is clear what exactly is being proved.

* TLAPS is one of the only systems that lets me number my equations - something I've done in, again, my 20 years of math training.

* TLA+ is not typed, unlike many others. This for me means that when writing my spec, I can just focus on my spec and not worry about types. Later, I will write a TypeInvariant and prove it. This is a personal preference. For eg, when proving problem P is NP-Complete, I don't want to care while specifying P that P is in NP. I will first specify P, then prove that P is in NP (and later NP-hard).

Best,

Saksham

[1] Harrison, John. "Proof style." International Workshop on Types for Proofs and Programs. Springer, Berlin, Heidelberg, 1996.

[2] Lamport, Leslie. "How to write a 21st century proof." Journal of fixed point theory and applications 11.1 (2012): 43-63.

[Apostolis Xekoukoulotakis]

I am not familiar with TLAPLUS, but with regards to the hierarchical structure of proofs that Leslie proposes, I think that it can also be done in Agda, but it requires the programmer to be thoughtful of the structure of the proof.(1)

(1) : https://lists.chalmers.se/pipermail/agda/2019/010798.html

--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Stephan Merz]

Hello,

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.

Regards,

Stephan

[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.