Systems Correctness Practices at Amazon Web Services

I particularly like the branding here as “systems correctness.” This allows you to slide around the formality spectrum, rather than just focusing entirely on formal verification vs. traditional testing. I think this middle area (so called “lightweight formal methods”) are what’s gaining a lot of traction, because of the inherent connection to implementation code.

While I don’t need to be sold on the benefits of design / protocol verification, it can be difficult to convince others of that. But I see people being much more open to PBT, DST, or runtime monitoring. That’s a pretty easy sell: “how many times have you written a ton of unit tests, but still ran into bugs in production?” There’s clearly more that can be done.

One thing I wondered about the P language: It seems like in the early days, it was used at Microsoft to generate C code that’s actually used at runtime in the Windows USB stack?

But now it is no longer used to generate production code?

I asked that question here, which I think was the same question as in a talk: https://news.ycombinator.com/item?id=34284557

It seems like if the generated code is used in a kernel, it could also be used in a cloud, which is less resource-constrained

---

I thought I saw an article going into detail about P and Windows USB, but I can’t find it anymore. This article is vague on whether the generated code is used:

https://www.opensourceforu.com/2016/10/microsoft-p-lanuguage-enables-safe-event-driven-programming/

Microsoft has additionally developed a P compiler that outputs a Zing model to enable systematic testing. The compiler also generates C code that can be used in a C compiler for execution.

And then on the home page https://github.com/p-org/P :

P was first used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone.

Is it a technique that could be adopted for open source operating systems?