An analysis of Runway from a TLA+ perspective

[Andrew Helwer]

Over at the tlaplus Google Group, I've posted my thoughts on Runway from a TLA+ perspective: link

Look forward to hearing your thoughts! The objective of my analysis was to answer the following questions:

1. In the areas where feature overlap exists, how does Runway compare to TLA+?
2. What additional features does Runway possess, and how/how well do they work?
3. What is the possible impact of Runway on formal specification in general and TLA+ in particular?

[Diego Ongaro]

Hey Andrew,

Thanks a lot for taking the time to share that. You were perhaps too generous with overlooking Runway's current immature state, but even if unfairly giving Runway the benefit of youth, the comparison is quite interesting. I think your conclusions are right, and I hope people over on the tlaplus list see it that way too. TLA+ and Runway "compete" for some segment of users where both tools would be suitable, but they have very similar mission statements. If the world adopts any tool in this space, that's going to be a win for everyone.

From the thread on the tlaplus list (up to now), I learned that, in some form or another, TLA+ can do simulation and visualization. That's pretty cool, and it speaks to the large ecosystem that's built up around TLA+. On the other hand, I bet the developer and user experience for these on Runway can be better, as these are core features being designed into Runway.

Another feature of Runway that I think is important is the ability to share models on https://runway.systems. There's no registry for them quite yet, but at least you can link people to models now. For example, here's a weird one (River) from Damian Gryski, and here's a model of BookKeeper that I wrote last Monday. I think that's pretty powerful, and I don't think most TLA+ models can be appreciated without either careful reading or installing a big software package.

It hadn't occurred to me before that Runway's REPL is an important feature. I guess it seemed like an obvious thing to do at the time, since Runway models look so much like programming languages. There's certainly a lot we could do to improve the REPL, too (think `python` vs `ipython`, and making the REPL in runway-browser more usable).

On the topic of pretty-printed specifications, I'm not sure I see this as a feature in TLA+. TLA+'s pretty printer renders special characters, but IMO the output is not as readable as syntax-highlighted code. And I see the special characters as harmful to TLA's learning curve, since they provide little hint of their meaning to those unfamiliar with them. I like the idea that I can read a Runway spec without rendering it into a PDF, and I'm a big fan of syntax highlighting. (I wrote a TLA+ highlight file for vim back in 2013, though it's mis-categorized as a color scheme).

BTW, as to writing a view for the Die Hard problem, it probably is a bit difficult to draw water pouring from one bucket to another. I have no experience with that, but you might have an easier time starting with the BookKeeper view (350 LOC) than the Raft one (800 LOC).

I'm replying on runway-dev rather than tlaplus probably because I'm biased towards the audience here and the goal here of improving Runway. Feel free to link/quote back on tlaplus if I you think there's interesting discussion to have over there. (I'm presently waiting for my membership request to be processed for tlaplus. I'm not going to put messages into the moderation queue before then; I'm too familiar with the issue of latency in distributed systems.)

-Diego