Re: [tlaplus] TLA+ for testing computational algorithms rather than verify mathematical proofs

["'Martin' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

Hello Marta!

Showing properties of algorithms is where TLA+ stands out from other logics / 
specification languages. The language itself is expressive enough to cover most 
of mathematics even when we disregard the temporal aspects though.

Which TLA+ statements we can prove depends on the tools we use. TLC enumerates 
all possible variable assignments. It is useful to find counterexamples and 
explore problems with finite state spaces. In engineering we might limit ourself 
to checking only a relevant finite amount of a problem with an infinite state 
space. In that case we don't get a proof of the statement but certainly more 
confidence than by classical testing.

TLAPS can prove statements of TLA+ in general, including purely mathematical 
statements. For example Stephan's mail yesterday contained links to actual 
proofs of Cantor's theorem.

What's so nice about TLA+ is that we can get already very far by just formally 
stating the problem and exploring it with TLC. Some people already stop there, 
others use TLAPS and add the proofs as well (proving is more time consuming than 
writing the problem down after all). That's why you can find both flavours - or 
even a mix of them - online.

cheers,
Martin


On 4/28/24 00:49, marta zhango wrote:
> Have been reading the book TLA+ of Hillel.  It is as though TLA+ is only
> useful
> to test computations algorithms.  One cannot test mathematical proofs.  Is
> this
> correct ?

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/79520297-12e7-4df4-99d0-51e6b1a1dc40%40gmail.com.