in the readme: (e.g. if the process will terminate or if the ).

Interesting — I’d quite like to use something like this; but my fear is that learning it would be harder than learning TLA+, as I’d need to learn both, and how one maps into the other. I’ve only dabbled in TLA+ and not enough to really grok it; but I do know clojure. What does this aim to make easier?

For someone new to the concept of a model checker - how does it compare to property-based testing?

I am attracted by the possibilities of model verification but I have never worked in the domain so I do not know many things, such as • As a backend clj developer, where I might use this in practice? • What is the least resistance way of getting productive with model checking? Do I need to learn TLA+? • What are the different approaches to model checking, their limitations and pros and cons => which is (not) suitable for my needs?

@U06BEJGKD: I’m no expert — but I think the main thing is that something like TLA+ aims to give you a proof of correctness for a model. Property testing doesn’t give you a proof of correctness; it just asserts that a given property holds for all tested inputs; of an implementation. i.e. the main differences to me seem to be in mathematical proof of correctness vs evidence of it… and also the difference between a model of a system and the system itself. A model being the thing you design and work on to get your thinking straight; before you engage in the implementation.

If your process was: 1. develop and prove a model. 2. build an implementation of that model 3. test the implementation Then one of the things you want to do is ensure the proofs of the model carry over into your implementation. i.e. you need something to assure the implementation is a faithful recreation of the proven model. I suspect there are many techniques to doing this; but I’d imagine one would be writing property tests of the implementation which are directly derived from your model.

Aha, that’s useful, thanks!

Thanks for answering @U06BEJGKD question, @U06HHF230! @U06HHF230 @U0522TWDA You don't need to learn the TLA+ language at all, the concepts will be similar (e.g. invariants, state, temporal properties) as we call TLC (the TLA+ model checker) behind the scenes, you just have to keep using Clojure (it does not transpile CLJ to TLA+, it's real CLJ!). You will use model checking in practice only if you feel something is kinda important for your business, you definitely shouldn't need to use it to model a CRUD API, but it would be good to model, for example, some custom protocol you have which replicates data and which can make you lose a lot of money if it violates some invariant. See the business case for when to use and not to use at https://www.hillelwayne.com/post/business-case-formal-methods/, Hillel also has a lot of great posts about TLA+ (besides his wonderful newsletter). The best book to initiate at Model Checking I know is the one from Hillel itself https://link.springer.com/book/10.1007/978-1-4842-3829-5, there is even a entire suite of tests based on the book at Recife so you can follow it in Clojure (https://github.com/pfeodrippe/recife/blob/master/test/hillel_test.clj). One big limitation of model checking is that, while you don't need to write a Math proof (which it takes a LONG time and lots of qualified personal), it brute forces all the possible states, so it may take a while to finish. There are ways to mitigate that, but only by using is that you will feel. For example, there is something called the Small Scope Hypothesis which says that if it works using 2 or 3 entities, then it's very likely that it will work with many, so you don't need to be crazy and test 10 servers with 20 queues (it increases exponentially the number of states).

Let me know if you have some other questions, it's an experiment and I would be happy to improve based on the community's feedback :)

> You don’t need to learn the TLA+ language at all, the concepts will be similar (e.g. invariants, state, temporal properties) Ok, but aren’t the best descriptions of these concepts and how to wield them going to be in resources that teach the TLA+ language?

Yes, Rick, absolutely, there are tons of resource out there for it in TLA+. There are some new model checkers, like the one in Rust, which also explain it beautifully https://docs.rs/stateright/0.28.0/stateright/. Others in Java, C# etc. For us it may suffice to say to start that an invariant is just an assertion about one state (a function) and a temporal property is an assertion about multiple states (a function + operators like always or eventually). But I agree we definitely need to work on documentation 😅, you can check about the concepts also at https://learntla.com/introduction.

Thanks for the links… It’s a big area, and figuring out an appropriate starting point / journey is part of the challenge. For example - previously I started with LL’s excellent video series… It was quite refreshing to see a turing award winner, not taking himself too seriously and dressing up randomly as a clown 😆 I went from there to playing around with the TLA+ IDE and tools, and trying out some examples… but my attention drifted onto other things. I guess I never quite got enough of an in, to figure out if what I was learning was appropriate for the problems I might apply it to.

i.e. was TLA+ even the right tool — or would I better with Idris or Coq?

Yeah, things are getting better in the TLA+ tooling, but it's slow progress, so I went to full Clojure with the ready to be used tools. Idris and Coq are much harder IMHO as you they lean into formal proofs, which takes WAAAY longer to build. They are complementary to model checker, but low ROI for most of the things we need to do in practice.

Nice to see you have some experience :)

I've created an issue so you can add questions if you want there and I will try to answer in the talk https://github.com/pfeodrippe/recife/issues/6. But you can keep asking me here o/

@rickmoynihan I also loved the LL videos. There was some meta humor in the fact that it was so apparent that he was attempting to move his listeners from state a to state b in a provable manner.. The displayed pattern of his process re-enforced the whole point of the curriculum.

What video series are you talking about? Sounds fun!

Probably https://youtube.com/playlist?list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD

Yes that’s the videos — though the website is slightly better and has links to supporting materials: http://lamport.azurewebsites.net/video/videos.html