This is very interesting. It seems like a much more user-friendly version of TLA+. Wonder what Lamport thinks about it :)
I think the next logical feature would be to have Runway compile a model-checked specification to an actual C++/Java/go/python implementation, using something like Thrift or CapnProto RPC codegen. There has been some work on doing similar spec->implementation compilation from Coq to erlang [0] but the author hit a lot of obstacles.
That is exactly the effort done in our group before (from TLA+ to real C++ implementation) - the challenge is that the gap between specification and the implementation is large in terms of both implementation details and language expressiveness. As a complementary approach, we have come up libraries for distributed system development with built-in implementation-level model checking support. You may check out https://github.com/Microsoft/rDSN for details.
Hmm, I find TLA+ to be very user-friendly. It's one of its major strengths (it was very important to Lamport to observe engineers as they learn and apply it). It is certainly easier than learning Haskell, or even OCaml or Rust. I think it's a bit like Lisp: it's a minimal language with very few concepts, that may be unfamiliar at first and take a bit to fully wrap your head around, but once you do, you have unlimited power. I think that you can become seriously productive in it after about two weeks. All the tricky concepts (the TLA part of TLA+) are explained in this very short text[1] (I haven't seen the operator introduced in the Assumption/Guarantee section used in a spec). When you get those, you know TLA+ well, the "+" bit is very easy; a little like Clojure, only simpler.
It's not only easy to learn, it's extremely powerful, mostly due to refinements (an advanced concept, better left for week 3 :)), which are absolutely necessary for large systems/algorithms.
There are also two breakthroughs in TLA, which you may come to appreciate: the expression of the program and the program's properties in the same minimal language, and the demonstration that simple, high-school math, plus one or two new concepts, is all it takes to specify and verify programs.
And yeah, code extraction from specification is an open research question, but I don't even consider this to be a top-ten desired feature, considering the amount of time spent specing and verifying vs. translating to the implementation language.
The Banana and Elevator demos did not specify/verify temporal properties so I suspect it doesn't support specifying temporal formulas at the moment (the T in TLA+). This means it can be used to check correctness properties but not liveness properties. Despite this limitation I believe this is a fantastic tool as it makes writing specs way more approachable.
I think the next logical feature would be to have Runway compile a model-checked specification to an actual C++/Java/go/python implementation, using something like Thrift or CapnProto RPC codegen. There has been some work on doing similar spec->implementation compilation from Coq to erlang [0] but the author hit a lot of obstacles.
[0] - http://christophermeiklejohn.com/coq/erlang/2013/11/19/verif...