Hacker News Reader

Comment by mooneater | Hacker News Reader

Can anyone comment on where exactly lies the line between, too simple to need formal specs, vs crazy to build it without them?

What would be the simplest system for which you would recommend taking the time to make a formal spec?

View on HN

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.

Awesome response, esp. the concrete example

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.

There are two parts to this: writing a spec and formalizing it.

Writing stuff down helps you organize, clarify and communicate your thoughts. You should write down a spec if you think the spec you hold in your mind can benefit from organization, clarification and communication at a level that's higher than the code.

Formal means mechanical. You should write a formal spec if you feel it is complex or subtle enough to benefit from machine-aided analysis. Code is a form of formal specification (it is a specification because it describes what the system does; it is formal as it is interpretable by a computer). But code is a formal specification at a very particular level of abstraction, that may not be convenient to answer your questions.

Some people think that high-level programming languages are convenient enough for the kind of analysis you want. Sometimes they are right, but often they are wrong. Explaining exactly why a language like TLA+ is more convenient than any programming language that exists or could ever exist requires some technical details (I've attempted to give a high-level explanation for why that is so here[1], but roughly, some useful levels of abstraction cannot possibly be compiled/interpreted -- as doing so in general is uncomputable -- but compilation/interpretation is a strong requirement of programming languages). However, a more concrete example of why code is insufficient is in the case of a distributed system, where you want to cocisely describe not just the behaviour of a single program, but the interaction among a set of communicating programs, the network environment and the behavior of the users (the last is relevant for any interactive system, which is a special case of a distributed one).

As a rule of thumb I'd say that algorithms/systems with any non-trivial amount of concurrency (i.e. concurrent algorithms/data structures and distributed systems) can greatly benefit from a formal specification. Sequential programs may also benefit, if there is a complex interaction of rules. For example, I saw a talk that suggests formalization of the tax code as a means to find inconsistencies[2], but a business system that encodes many interacting business rules could also benefit.

[1]: https://pron.github.io/posts/tlaplus_part3#algorithms-and-pr...

[2]: https://youtu.be/EshxZVMURt4

Reply on news.ycombinator.com