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

*From*: saksha...@xxxxxxxxxxxxxx*Date*: Tue, 5 Feb 2019 16:19:41 -0800 (PST)*References*: <4550f6e3-ace6-4e2a-a6d6-b379e7ebbb68@googlegroups.com>

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

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

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.

Regards,

Roberto

**Follow-Ups**:**Re: [tlaplus] Re: Comparison between TLAPS and other proof assitants***From:*Apostolis Xekoukoulotakis

**References**:**Comparison between TLAPS and other proof assitants***From:*Roberto

- Prev by Date:
**Re: Practical TLA+ now out** - Next by Date:
**Re: How does Fairness relate to the State Graph** - Previous by thread:
**Comparison between TLAPS and other proof assitants** - Next by thread:
**Re: [tlaplus] Re: Comparison between TLAPS and other proof assitants** - Index(es):