[blorgle]

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]

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.

[iheartmemcache]

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?

[Kaizyn]

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.

[ulber]

"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.