Why Specifications Don't Compose
hillelwayne.com
Why Specifications Don't Compose
1–10 of 65 posts
Re: Why Specifications Don't Compose
#2Please change title to reflect that this is not about "specifications" in the more common usage and is about formal methods.
Re: Why Specifications Don't Compose
#3Please change title to reflect that this is not about "specifications" in the more common usage and is about formal methods.
What is the “more common usage” of the word “specifications”, for example?
Re: Why Specifications Don't Compose
#4Please change title to reflect that this is not about "specifications" in the more common usage and is about formal methods.
What is the “more common usage” of the word “specifications”, for example?
I read this as the "specifications" in "requirements and specifications" for e.g. software projects. For example, "there should be a button that pulls in new data when clicked". That's generally pretty different from formal/mathematical specifications.
Re: Why Specifications Don't Compose
#5This post is about stateful formal methods. Formal methods can also be used with functional programming, right? Is it any easier to compose specifications in that case?
Re: Why Specifications Don't Compose
#6Earlier quoted context omitted.
What is the “more common usage” of the word “specifications”, for example?
I read this as the "specifications" in "requirements and specifications" for e.g. software projects. For example, "there should be a button that pulls in new data when clicked". That's generally pretty different from formal/mathematical specifications.
Even those kinds of specifications don't compose well. For instance, if you have a solved problem, and you add a requirement, you don't really have a solved problem anymore, and the new solution may look extremely different from the old one.
Re: Why Specifications Don't Compose
#7Ah, universal composition... the mother of complexity. Seems like the standard approach, in all manifestations of composed systems, is to find some property that makes composition “work” and then sandbox or guardrail the real system to (1) ensure the property holds in practice, and (2) recover without too much collateral damage when it fails to hold.
Of course there are no black boxes in the real world, but the staggering hierarchical complexity of life would seem to indicate that one can engineer systems (whether natural or man-made) that are close enough to be indistinguishable.
Re: Why Specifications Don't Compose
#8Earlier quoted context omitted.
What is the “more common usage” of the word “specifications”, for example?
I read this as the "specifications" in "requirements and specifications" for e.g. software projects. For example, "there should be a button that pulls in new data when clicked". That's generally pretty different from formal/mathematical specifications.
I’d suggest that they are in fact the same thing, and differ only in the level of formality... somewhat akin to the difference between machine code and interpreted scripts.
Re: Why Specifications Don't Compose
#9Earlier quoted context omitted.
What is the “more common usage” of the word “specifications”, for example?
I read this as the "specifications" in "requirements and specifications" for e.g. software projects. For example, "there should be a button that pulls in new data when clicked". That's generally pretty different from formal/mathematical specifications.
Uhm, are they that different, though?
For instance, you can formally express at least a part of the "there should be a button that pulls in new data when clicked" specification. In LTL, that would be something like something like:
[] (buttonClicked -> newDataPulled)
(Notice that I switched from actions (click, pull) to states (clicked, pulled), as LTL is a state-based logic.)
Re: Why Specifications Don't Compose
#10Earlier quoted context omitted.
I read this as the "specifications" in "requirements and specifications" for e.g. software projects. For example, "there should be a button that pulls in new data when clicked". That's generally pretty different from formal/mathematical specifications.
Uhm, are they that different, though? For instance, you can formally express at least a part of the "there should be a button that pulls in new data when clicked" specification. In LTL, that would be something like something like: [] (buttonClicked -> newDataPulled) (Notice that I switched from actions (click, pull) to states (clicked, pulled), as LTL is a state-based logic.)
Yes.
E.g. according to the article "Specs are math" <-- not in my experience