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

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

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.


On 4/28/24 00:49, marta zhango wrote:
Have been reading the book TLA+ of Hillel.  It is as though TLA+ is only
to test computations algorithms.  One cannot test mathematical proofs.  Is
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.