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

Post by rurban » Mon, May 22, 2017, 5:06 AM UTC

staticassertion wrote: post #12

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 -…

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.

Post by Kaizyn » Mon, May 22, 2017, 12:51 PM UTC

iheartmemcache wrote: post #26

mmalone wrote: post #17

Earlier quoted context omitted.

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…

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 in…

Lamport isn't behind the P language, and it isn't as expressive as TLA+ so it isn't a replacement for his work in that area.

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

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