This seems to be a modern alternative to TLA+ (unless I’m misunderstanding something). Is anyone familiar with the pros/cons between the two? I was hoping to see a comparison page on the site but didn’t see one.
I don’t know enough about the two technologies yet to comment. Although DS is an area I’m passionate about, I am still learning about the FM approaches to these sorts of problems.
TLA+ checks the entire state space of an algorithm. P explores the state space of a program guided by some random strategy. TLA+ can be used to prove an algorithm is correct, while P is just a test tool. Recently I’m working to verify the design of a storage system at work. I tried to specify a simple version of the design in PlusCal which transpiles to TLA, but blocked by the state explosion problem (TLA+ checker runs out of memory and too slow). Then I switched to P. P allows me to put more details of the system into the specification. The state space is even larger than the PlusCal version. But P does not exhaust all the states during test. Usually I run a few hundreds of thousands of test iterations to ensure there is no big issue in the design. P also looks much familiar to an average programmer.