5 ms·

I think we need reusable (formal) specifications for it to become adapted widely. If that could be done in a way similar to how we today use open source librari

I think we need reusable (formal) specifications for it to become adapted widely. If that could be done in a way similar to how we today use open source libraries of reusable code, findable via a package manager, it might fly. Writing formal specs from scratch each and every time is too time consuming relative to the gain, except for in a few critical usecases.

settler4 8y ago
And then find a way to run that and so turn it into a programming language?
- jononor 8y ago
  No we already have enough of those. But one could implement a way of annotating that some code/package (in ordinary programming language) implements a certain specification. This metadata should be searchable through the package manager.
  - emodendroket 8y ago
    What, like WCF?
pron 8y ago
If you use TLA+ you'll see why this is likely unnecessary. A huge specification, made at three levels of detail, can run to 2500 LOC. Because you have so much control over the level of detail, and because the language is so expressive, there is little need for reuse (except maybe for some common definitions, e.g. of different consistency levels, which are very short but can be non-trivial).
- jononor 8y ago
  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 effort be encapsulated into something reusable? The desire for reuse is not driven by a want to reduce LOC, but hours spent.
  - 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.

settler4 8y ago

And then find a way to run that and so turn it into a programming language?

jononor 8y ago
No we already have enough of those. But one could implement a way of annotating that some code/package (in ordinary programming language) implements a certain specification. This metadata should be searchable through the package manager.
- emodendroket 8y ago
  What, like WCF?

pron 8y ago

If you use TLA+ you'll see why this is likely unnecessary. A huge specification, made at three levels of detail, can run to 2500 LOC. Because you have so much control over the level of detail, and because the language is so expressive, there is little need for reuse (except maybe for some common definitions, e.g. of different consistency levels, which are very short but can be non-trivial).

jononor 8y ago
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 effort be encapsulated into something reusable? The desire for reuse is not driven by a want to reduce LOC, but hours spent.
- 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.