Hacker News Reader

Comment by colanderman | Hacker News Reader

I readily use TLA+ or PlusCal whenever I am reasoning about a system which may (if buggy) experience deadlock, starvation, race conditions, etc. This includes most systems involving two or more communicating processes. (The exceptions are those systems, such as a simple pipeline, where communication is trivial and acyclic.)

It's perfectly suited to this domain of problems, which also happen to be those which are difficult for humans to reason about (owing to the sheer number of possible interleavings of execution between two or more processes).

And TLA+, an especially PlusCal, are simple enough that no system is really "too small" to be modeled. E.g. a PlusCal model of a simple pipelined server (say, reading stuff from the network and writing asynchronously to disk) is maybe ¼ to ½ the size of the actual implementation, with half as much again worth of invariants.

View on HN

Exactly what I was feeling in my gut... but then what is the overwhelming advantage over rust that as far as I know is designed specifically for this kind of problems but is much easier to reason about, at least coming from standard programming?

Rust is much less expressive (meaning, it is not able to say many interesting things about the system) and far harder to reason about than the much simpler and more expressive (though less familiar an un-compilable) TLA+. In fact, here[1] is some work by someone who designs concurrent/distributed algorithms in TLA+ and implements them in Rust.

This is not a shortcoming of Rust in particular. No programming language can be as expressive and as simple as a specialized specification language like TLA+ (it could be by essentially embedding a specification language in some specification tier of the language -- like the type level in languages with dependent types like Idris or the contract level like languages with formal contracts like Java with JML or SPARK, but this comes at the cost of either less expressive power and/or much increased complexity)

[1]: https://github.com/spacejam/tla-rust

What happens when your Rust has coordinate with an unreliable vendor system written in QBasic? What if a sensor is affected by bad weather? What if there are malicious clients? With specification, we can talk about systems in a wider context than just individual programs.

The primary benefit of TLA+ over any general-purpose language is that it – as a modeling language – allows you to elide those parts of your system that "don't matter". To continue my earlier server example, when modeling, I probably don't care specifically which functions I'm using to read data from the network, under what conditions they produce which errors, or how the OS might decide to schedule them. I just care that such a function exists, that it may error out, and that it gets scheduled somehow.

Then, as a consequence of clearly expressing all the behaviors my system might express, TLC (the TLA+ model checker) is able to exhaustively search these possibilities for bugs. This is at best intractable for any system where you are unable to abstract out the things that "don't matter", like in Rust. There are just too many variables (literally) in the search space.

That said, there's nothing particularly special about TLA+, or especially PlusCal. They just provide language features such as first-class sets and clearly-defined atomic state transitions that make it very easy to describe a system without too much irrelevant "stuff". The only particularly notable feature of the modelling portion of the languages is nondeterminism, which is necessary to express the boundaries of your model (e.g. nondeterminism is how you model the "receive from network" function as "a function that either returns some data or throws some error").

One could even imagine using Rust (to use your example) as a modeling language. You'd need to add nondeterminism (or another means of specifying contracts), and a way to specify temporal invariants to check. And also annotate which functions act as mutexes and which may block waiting for I/O. And you'd probably want to stub out container types so the model checker doesn't have to model their implementations. But once you've done all that, your mutant Rust is starting to look a heck of a lot like PlusCal, only more complicated.

Doing the comparison TLA vs Rust as programming languages is a misunderstanding. It's exactly equivalent to the misunderstanding in a comparison like "what's the advantage of SQL over Rust, that as far as I know is designed specifically for this kind of problems". Now, one could believe, perhaps, that Rust is "designed specifically" for the implementation of database "kind of problems". But the conclusion that there is therefore no "overwhelming advantage" to databases would not follow from that belief.

TLA and the TLA tools form a model checker. The TLA language is not used to do computations,but, rather, is used to describe properties and behavior of complex systems. The TLA tools then machine validate the descriptions to assure that the evolution of a system with the given behaviors will satisfy expected correctness properties. A TLA specification tells you that if your system is implemented (in a computer language, like say Rust) according to the description then the systems operation will satisfy the validated correctness properties.

TLA is about answering the question "Do I properly understand my problem and will my solution logic satisfy problem needs?". Rust doesn't help answer that question.

Awesome response, esp. the concrete example

Reply on news.ycombinator.com