Why CSP matters I: Keeping things in sync (2016)

The FDR4 checker [1] looks pretty slick. I'm not that familiar with the area, though, so I'm wondering how it compares to model checkers? How does using a model checker compare to using a refinement checker? (I've read that there are model checkers for TLA+.)

[1] https://www.cs.ox.ac.uk/projects/fdr/

I wonder if the real solution here is just better UX... The WhatsApp model for message delivery gives visual confirmation when a message is sent, and then more once it's been ACK'ed by the receiver's phone. This manages the uncertainty, instead of trying to solve it. I know that my change to the grocery list isn't 'real' until I've gotten ACKs back from everyone.

Differential sync is not a very clean solution, because it doesn't encode the intention of differences.

If one person increments a variable from 10 to 11, and another person sets the variable from 10 to 11 independently, does that mean that the final value should be 11 or 12?

Of course, in practice, you can work around cases like this. It is just not very clean and feels like a hack.

Saw "CSP" and immediately thought of constraint satisfaction problems [0].

Unfortunate acronym.

[0] https://en.wikipedia.org/wiki/Constraint_satisfaction_proble...