My team at AWS has been using P heavily for modelling and reasoning about distributed storage and database protocols and designs. I'm a big fan. The sweet spot for P in my mind comes from the fact that it's a much more approachable language, and mental model, than TLA+ (or Pluscal) for most programmers. That means that folks can pick up formal verification more easily, and then expand into tools like TLA+ or Dafny as their needs change.
I find myself reaching for P when, in the past, I would have reached for Pluscal. TLA+ is still my go-to for more "conceptual" problems, but I find the state machine model in P perfect for cloud systems work.
Ankush Desai did a great talk at HPTS'22 about P, and finding critical distributed systems bugs early: http://hpts.ws/papers/2022/HPTS2022.pdf He's also been working on some very interesting new directions for the verifier, and for closing the gap between specification and implementation for systems that are specified using P.
They've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify the actual system source code).
If you don't show me the syntax above the fold on first page view, I'm something like 50% more likely to disregard. I know this has false positives associated, but I don't entirely feel in the wrong for this either.
Indeed, they hid source code samples a bit too deep.
Easiest I could find is to go to tutorials in the menu, for instance, [1]. Such pages have links to actual source files which live on GitHub, like [2].
I love ideas like this. It's "top-down" programming: start with a high-level, formal description of the system. ("There are 4 communicating state machines."). Then you gradually add detail to the model and go "downwards" until you reach the level where you can actually generate code.
Yep agree. It’s a great way to write solid software. You can do something similar even when not using formal methods:
Start by writing the skeleton of the complete application. By “skeleton” I mean all interfaces implemented with placeholder all-in-memory code. And then step-by-step refine the whole application until it is done.
I was surprised, because from a performance perspective, I'd expect that if you can generate code for USB drivers, you can also do so for cloud services? You have generally have better and more control over hardware in the latter case?
The state machines seem pretty low level, so I don't see in principle why efficient code couldn't be generated from them.
Is it an issue of wanting the implementations to use many cores perhaps?
I wonder if the P-generated code is still used for USB drivers today, or if they moved away from that approach and just use the modeling process?
Thanks for any clarification
FWIW I'm using 3 or 4 C/C++ code generators for https://www.oilshell.org, and I've the layer of indirection useful in many ways (although it also can make it harder for people to understand)
Yes, P has been updated a lot in the last 6 years. Much better documentation and compiler. There is going to be a new release in a couple of months with a verifier as well as a way to check P specifications on implementation.
Can someone provide a simple hello world example of a program in P? I searched the website. It provides definitions and ideas for many concepts. But not a single example.
This title doesn't really tell the reader what the P language is for.
dang, would it be possible to change the title to something like, "P Language: a state machine-based programming language" ? (That's from the first diagram on the page.)
I find myself reaching for P when, in the past, I would have reached for Pluscal. TLA+ is still my go-to for more "conceptual" problems, but I find the state machine model in P perfect for cloud systems work.
Ankush Desai did a great talk at HPTS'22 about P, and finding critical distributed systems bugs early: http://hpts.ws/papers/2022/HPTS2022.pdf He's also been working on some very interesting new directions for the verifier, and for closing the gap between specification and implementation for systems that are specified using P.