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
It looks like Coyote[0], which is used in azure, was an evolution of P# which was an evolution of P
[0]https://www.microsoft.com/en-us/research/wp-content/uploads/...
+1.
We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.