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