2 ms·

How do you mean unnecessary? Surely writing such a specification takes many man hours, even after having spent many man hours to learn TLA+? Can none of this e

• pron 8y ago
  Most of the effort writing TLA+ is about the what not the how. In general, we know how to make code reuse effective when a lot of implementation hides behind a thin API, but in TLA+ there is no implementation in a meaningful sense. A library of requirements would make about as much sense, and while maybe it's something that could be done, I'm not sure we know how to do it (but if you've seen something like it, I'd love to see it). So maybe it's an interesting idea, but I'm not sure how it would be done. Aside from a utility module that I like including in most of my specs, I never "reuse" modules as is. I often do, however, copy-paste-modify pieces of other specifications, which, I assume, is not unlike how lawyers reuse portions of contracts. I guess there are occasionally pieces that could be used as-is (e.g. a description of a lossy network), but those tend to be so simple, that looking for them in some Maven-central for spec modules would probably more effort than writing them from scratch every time.