6 ms·

P: A programming language for asynchrony, fault-tolerance and uncertainty

266 points by JulienRbrt 9y ago

sverige 9y ago
At last, the long awaited successor to C, at least in the naming convention that assumes P comes after C because of BCPL. (Apologies to Walter Bright: No inference should be drawn that D was not also a good name for that sequence.)
- nickpsecurity 9y ago
  It's a language for expressing protocols. So, P for protocols most likely. It also focuses on safety and ease of analysis. Can't possibly be connected to the C lineage...
  - girvo 9y ago
    I believe it does compile to C, interestingly, so not really connected, but a little bit nonetheless
- mattnewton 9y ago
  L must be lisp, brought here from the future by the space aliens.
  - Razengan 9y ago
    Or Logo.
- contingencies 9y ago
  https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation
panic 9y ago
It's worth noting that this isn't just a research language -- it's used in practice for writing drivers: P got its start in Microsoft software development when it was used to ship the USB 3.0 drivers in Windows 8.1 and Windows Phone. These drivers handle one of the most important peripherals in the Windows ecosystem and run on hundreds of millions of devices today. P enabled the detection and debugging of hundreds of race conditions and Heisenbugs early on in the design of the drivers, and is now extensively used for driver development in Windows.
- blorgle 9y ago
  This looks SO cool! Kind of like Erlang but at a different level, so you can model both inter-node systems (like Erlang) but also intra-node systems (like USB3 drivers)! As someone who has been thinking a lot recently about SPARK/Ada and "free" formal verification, can anyone tell me how this language compares on that front? If I write a P program, do I get the ability to "prove" its correctness?
  - mmalone 9y ago
    The docs are sparse... but it looks like the answer is that it depends on what you mean by "correct." It doesn't look like it's a general purpose theorem prover, but it does appear to be model/spec-driven and the linked article says that the system can prove safety and liveness. I'm guessing they mean "type safety" but they may be using the term in the broader distributed system sense. In any case, it does look like it gives you certain "proofs for free" if your definition of correct is "eventually converges on a consistent state." I don't think you can prove arbitrary properties like you can with Coq or with a dependent type system. Still, very cool.
    - ulber 9y ago
      "Safety" in a verification context generally refers to safety properties, i.e., properties that can be shown to not hold with a finite counter example (a test that hits a bug). Liveness properties in comparison are those that need an infinite counter example, i.e., a way to make the bad thing happen infinitely often.
    - iheartmemcache 9y ago
      You can if you want to go that 'far'. It's pretty easy to add full SMT support if you want (via Z3). Out of the box, it's not required. You get existential/universal quantification, conjunction and disjunction as your dyads, and invariance properties out of the box. I'm guessing Lamport chose not to go the 'fully dependent' route Coq/Agda style (based on his presentation at least) because, well, as he said in the intro lecture - engineers don't really want formal verification at that level but still want strict invariants of their system to be ensured s.t. you can be guaranteed your program will never enter an undefined state nor encounter any undefined behavior as a result entering into an ill-defined state and proceeding to get UB (or 'implementation-specific', ugh) as a result. What really drove it home is reading the paper Lamport referenced, "How Amazon Web Services Uses Formal Systems" (Newcombe, et al, 2015) along with his RTOS anecdote of decreasing their NASA RTOS' KLOC by 10x while getting stronger guarantees in the process (see: "Formal Verification of a Network-Centric RTOS", Verhulst et al, 2011). It's also got more than a few similarities with "Fortress". Guy Steele really pushed this programming model while at Sun, but sadly DARPA killed the funding for it. That being said, Amazon has this is at > 14 of their AWS programs so it seems to be accessible and useful enough to the average engineer rather than 3 post-docs locked-up in their academic ivory tower, leaving twice a year only to present at ICFP and POPL. At the 'formal level', I think the closest analogue to the strength of your guarantee is either Ada/SPARK or QuickCheck. Certainly way stronger than your standard "oh hey, I wrote a unit test in an untyped language, I'm good to go!". (I.e., declare your give me your invariants and I'll make sure your system never reaches a state you don't want). Worth checking out if only because, hey, Lamport, Paxos. Have a look at Newcombe2015. It's only 8 pages, throw it on the Kindle or iPad, grab a coffee and have a go. What've you got to lose, right?
rubyn00bie 9y ago
If anyone is interested in syntax and more tangible bits, here is the manual from the GitHub page linked to in the article: https://github.com/p-org/P/blob/master/Doc/Manual/pmanual.pdf https://github.com/p-org/P/blob/master/Doc/Manual/pmanual.pd...
- tyingq 9y ago
  That would have been really helpful for things like telnet and option negotiation. Or more recently, perhaps something like QUIC.
tekacs 9y ago
Previous discussion: https://news.ycombinator.com/item?id=12673739 https://news.ycombinator.com/item?id=12673739
rambodroneprog 9y ago
P is also being used to build safe robotics systems. https://drona-org.github.io/Drona/ https://drona-org.github.io/Drona/
rambodroneprog 9y ago
The high-level syntax of the language looks amazing for writing and specifying complex protocols.
staticassertion 9y ago
P is a really cool language, and I've been keeping an eye on it. Unfortunately, the documentation has been pretty perpetually out of date, and the language is still a moving target. So you can't just "get started" in P, the example code won't compile. I don't know what their plans are or if they ever intend for it to be consumed outside of MS. If they do, some focus on docs would be nice. Pony is a similar language - but better documented. If you're interested in P, I suggest checking out Pony.
- rurban 9y ago
  Pony generates also much tighter, better, faster code. Code which I would use in a driver. Not managed C#. I know no other language which generates faster code. I mean faster than C++ with OpenMP, while being memory and concurrency safe. P has fantastic proof and test generating libraries and IDE's though. In pony you'll have to write perfect code to pass the type checker. P does much better handholding to get there.
robertkrahn01 9y ago
Here is a demo for using P to program a drone, shows a little more of the language itself: https://www.youtube.com/watch?v=R8ztpfMPs5c https://www.youtube.com/watch?v=R8ztpfMPs5c
- StreamBright 9y ago
  Thanks for sharing, this is really insightful.
- eggy 9y ago
  The graph visualization towards the end of the video in MS VS is amazing. I can see this being really useful for my robotics projects. I'll have to figure out how to get started. I was learning Erlang, and looked briefly at Pony, but the syntax and the demo appeals to me.
cgb223 9y ago
I'm still holding out for NP It'll be wayyy more complex
- moomin 9y ago
  (Citation needed)
tobyhinloopen 9y ago
Can we stop naming programming languages with letters and symbols and give it proper names that, when googled (or binged), makes the programming language appear on top?
- neokrish 9y ago
  Second this. It might seem irrelevant for us folks, we aware of different places to seek help e.g. Stackoverflow but when introducing someone new and they encounter a million questions about programming in a language, searching just becomes a nightmare with these single letter naming.
- LeoNatan25 9y ago
  Searching for "<Letter> Programming Language" works wonders. Give it a try sometime.
- progx 9y ago
  Plang
- mrslave 9y ago
  Someone uses Bing? And enough people to justify a new verb? binged is already taken and I don't think Microsoft wants to associate itself with such indulgence.
- paulddraper 9y ago
  So no B, C, or D? What about common words like Java, Ruby, Python, Go? I suppose this makes Scala and Perl the easiest languages to find documentation for.
faragon 9y ago
Microsoft's "Node.js" equivalent for asynchronous stuff?
deleted 9y ago
[deleted]
mempko 9y ago
Love it. What if all computing are communicating state machines

266 points by JulienRbrt 9y ago

At last, the long awaited successor to C, at least in the naming convention that assumes P comes after C because of BCPL. (Apologies to Walter Bright: No inference should be drawn that D was not also a good name for that sequence.)

nickpsecurity 9y ago
It's a language for expressing protocols. So, P for protocols most likely. It also focuses on safety and ease of analysis. Can't possibly be connected to the C lineage...
- girvo 9y ago
  I believe it does compile to C, interestingly, so not really connected, but a little bit nonetheless
mattnewton 9y ago
L must be lisp, brought here from the future by the space aliens.
- Razengan 9y ago
  Or Logo.
contingencies 9y ago
https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation

panic 9y ago

It's worth noting that this isn't just a research language -- it's used in practice for writing drivers: P got its start in Microsoft software development when it was used to ship the USB 3.0 drivers in Windows 8.1 and Windows Phone. These drivers handle one of the most important peripherals in the Windows ecosystem and run on hundreds of millions of devices today. P enabled the detection and debugging of hundreds of race conditions and Heisenbugs early on in the design of the drivers, and is now extensively used for driver development in Windows.

blorgle 9y ago
This looks SO cool! Kind of like Erlang but at a different level, so you can model both inter-node systems (like Erlang) but also intra-node systems (like USB3 drivers)! As someone who has been thinking a lot recently about SPARK/Ada and "free" formal verification, can anyone tell me how this language compares on that front? If I write a P program, do I get the ability to "prove" its correctness?
- mmalone 9y ago
  The docs are sparse... but it looks like the answer is that it depends on what you mean by "correct." It doesn't look like it's a general purpose theorem prover, but it does appear to be model/spec-driven and the linked article says that the system can prove safety and liveness. I'm guessing they mean "type safety" but they may be using the term in the broader distributed system sense. In any case, it does look like it gives you certain "proofs for free" if your definition of correct is "eventually converges on a consistent state." I don't think you can prove arbitrary properties like you can with Coq or with a dependent type system. Still, very cool.
  - ulber 9y ago
    "Safety" in a verification context generally refers to safety properties, i.e., properties that can be shown to not hold with a finite counter example (a test that hits a bug). Liveness properties in comparison are those that need an infinite counter example, i.e., a way to make the bad thing happen infinitely often.
  - iheartmemcache 9y ago
    You can if you want to go that 'far'. It's pretty easy to add full SMT support if you want (via Z3). Out of the box, it's not required. You get existential/universal quantification, conjunction and disjunction as your dyads, and invariance properties out of the box. I'm guessing Lamport chose not to go the 'fully dependent' route Coq/Agda style (based on his presentation at least) because, well, as he said in the intro lecture - engineers don't really want formal verification at that level but still want strict invariants of their system to be ensured s.t. you can be guaranteed your program will never enter an undefined state nor encounter any undefined behavior as a result entering into an ill-defined state and proceeding to get UB (or 'implementation-specific', ugh) as a result. What really drove it home is reading the paper Lamport referenced, "How Amazon Web Services Uses Formal Systems" (Newcombe, et al, 2015) along with his RTOS anecdote of decreasing their NASA RTOS' KLOC by 10x while getting stronger guarantees in the process (see: "Formal Verification of a Network-Centric RTOS", Verhulst et al, 2011). It's also got more than a few similarities with "Fortress". Guy Steele really pushed this programming model while at Sun, but sadly DARPA killed the funding for it. That being said, Amazon has this is at > 14 of their AWS programs so it seems to be accessible and useful enough to the average engineer rather than 3 post-docs locked-up in their academic ivory tower, leaving twice a year only to present at ICFP and POPL. At the 'formal level', I think the closest analogue to the strength of your guarantee is either Ada/SPARK or QuickCheck. Certainly way stronger than your standard "oh hey, I wrote a unit test in an untyped language, I'm good to go!". (I.e., declare your give me your invariants and I'll make sure your system never reaches a state you don't want). Worth checking out if only because, hey, Lamport, Paxos. Have a look at Newcombe2015. It's only 8 pages, throw it on the Kindle or iPad, grab a coffee and have a go. What've you got to lose, right?

rubyn00bie 9y ago

If anyone is interested in syntax and more tangible bits, here is the manual from the GitHub page linked to in the article: https://github.com/p-org/P/blob/master/Doc/Manual/pmanual.pdf https://github.com/p-org/P/blob/master/Doc/Manual/pmanual.pd...

tyingq 9y ago
That would have been really helpful for things like telnet and option negotiation. Or more recently, perhaps something like QUIC.

tekacs 9y ago

Previous discussion: https://news.ycombinator.com/item?id=12673739 https://news.ycombinator.com/item?id=12673739

rambodroneprog 9y ago

P is also being used to build safe robotics systems. https://drona-org.github.io/Drona/ https://drona-org.github.io/Drona/

rambodroneprog 9y ago

The high-level syntax of the language looks amazing for writing and specifying complex protocols.

staticassertion 9y ago

P is a really cool language, and I've been keeping an eye on it. Unfortunately, the documentation has been pretty perpetually out of date, and the language is still a moving target. So you can't just "get started" in P, the example code won't compile. I don't know what their plans are or if they ever intend for it to be consumed outside of MS. If they do, some focus on docs would be nice. Pony is a similar language - but better documented. If you're interested in P, I suggest checking out Pony.

rurban 9y ago
Pony generates also much tighter, better, faster code. Code which I would use in a driver. Not managed C#. I know no other language which generates faster code. I mean faster than C++ with OpenMP, while being memory and concurrency safe. P has fantastic proof and test generating libraries and IDE's though. In pony you'll have to write perfect code to pass the type checker. P does much better handholding to get there.

robertkrahn01 9y ago

Here is a demo for using P to program a drone, shows a little more of the language itself: https://www.youtube.com/watch?v=R8ztpfMPs5c https://www.youtube.com/watch?v=R8ztpfMPs5c

StreamBright 9y ago
Thanks for sharing, this is really insightful.
eggy 9y ago
The graph visualization towards the end of the video in MS VS is amazing. I can see this being really useful for my robotics projects. I'll have to figure out how to get started. I was learning Erlang, and looked briefly at Pony, but the syntax and the demo appeals to me.

cgb223 9y ago

I'm still holding out for NP It'll be wayyy more complex

moomin 9y ago
(Citation needed)

tobyhinloopen 9y ago

Can we stop naming programming languages with letters and symbols and give it proper names that, when googled (or binged), makes the programming language appear on top?

neokrish 9y ago
Second this. It might seem irrelevant for us folks, we aware of different places to seek help e.g. Stackoverflow but when introducing someone new and they encounter a million questions about programming in a language, searching just becomes a nightmare with these single letter naming.
LeoNatan25 9y ago
Searching for "<Letter> Programming Language" works wonders. Give it a try sometime.
progx 9y ago
Plang
mrslave 9y ago
Someone uses Bing? And enough people to justify a new verb? binged is already taken and I don't think Microsoft wants to associate itself with such indulgence.
paulddraper 9y ago
So no B, C, or D? What about common words like Java, Ruby, Python, Go? I suppose this makes Scala and Perl the easiest languages to find documentation for.

faragon 9y ago

Microsoft's "Node.js" equivalent for asynchronous stuff?

deleted 9y ago

[deleted]

mempko 9y ago

Love it. What if all computing are communicating state machines