Differences between TLA+ Specification and Property Based Testing

Hi Folks,

First time poster, and newbie^1 to both TLA+ and property based testing (PBT from here on out), generally. Recently, a blog post was published (http://nchammas.com/writing/how-not-to-die-hard-with-hypothesis) about solving the Die Hard 3 Jug problem in Hypothesis (http://hypothesis.works)--a PBT library for Python. The fact that this was so straightforward was rather shocking to me, I have to admit!

It seems to me that the main advantage TLA+ / Pluscal has over PBT is the high-level mathematical pseudocode... But a few questions about this assumption:

1. The Jug implementation in Hypothesis shows that for *some* specifications, TLA+ and PBT are equivalent in what can be expressed / specified / assured. Is this *generally* true?

2. I'm thinking that the concurrency support in TLA+ might also be a huge advantage, but I think it's likely possible to simulate this in PBT, as well. Is there anything special about TLA+'s concurrency modeling that couldn't be replicated via PBT?

3. Generally, why should someone choose TLA+ over PBT? What other advantages does TLA+ have over PBT?

4. I think it's the case that intuition on creating invariants and properties for specifications / PBT tests, comes with experience. But, what tips do y'all have for recognizing (learning to intuit) that these types of specifications can have meaningful impact on code that I'm writing every day (mostly around distributed systems monitoring, REST APIs)?

Thanks for your time!

Andrew "Overjoyed by the potential of this stuff to make everything I touch better" Gwozdziewycz

[^1]: Meaning, I've read the AWS paper, watched the Leslie Lamport lecture series (1-3), the DrTLA Paxos lecture, and read through some specifications in the tlaplus github repo. For both TLA+, and PBT, I have some clarity in how I'd use it for testing certain types of algorithms, but have no clue yet how to apply either to work I generally do.