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

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

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

On Wed, Feb 6, 2019 at 2:19 AM <saksha...@xxxxxxxxxxxxxx> wrote:
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).


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

On Tuesday, February 5, 2019 at 8:38:23 AM UTC-5, Roberto 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.