Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why Specifications Don't Compose

hillelwayne.com

Post reply on HN
Print view View original

31–40 of 65 posts

Re: Why Specifications Don't Compose

#31

Post by kgwxd »

ahelwer wrote: post #24
tlarkworthy wrote: post #19

I am not convinced. There is no justification for specification languages to insist on a single global namespace with no option for namespacing. Just coz an operator doesn't compose does not undermine the usefulness that some things do compose, and that namespacing and scopes are generally useful organisation and communication techniques. The only reason why LTL is in a global namespace is pure legacy inertia. Academ…

Can you describe how a formal specification system with namespacing would work?

Clojure Spec has it https://clojure.org/about/spec#_global_namespaced_names_are_...

Re: Why Specifications Don't Compose

#32

Post by simiones »

neel_k wrote: post #15
MaxBarraclough wrote: post #5

This 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?

For behavioural correctness of terminating functional programs, you can by and large treat your programs as plain mathematical functions. Then reasoning about them is as easy (or more likely, as hard) as ordinary math. If you want to reason about the performance of functional programs, or about the behaviour of imperative/concurrent programs, then you need more sophisticated techniques. But even in this case, specifi…

But the article doesn't deal with the possibility/impossibility of verification at all. It deals with the fact that (some?) specifications don't compose elegantly.

That is, that a sufficient specification for System A and a sufficient specification for System B can't be trivially composed into a sufficient specification for a System C = System A + System B. That's not to say that System C can't be specified, but that it can't be specified without re-creating the specifications for System A and System B.

Re: Why Specifications Don't Compose

#34

Post by maweki »

chriswarbo wrote: post #16
maweki wrote: post #11

Earlier quoted context omitted.

Now you have to talk about what a specification is. If it is a relation from some function input to its output, that would be one step. And of course, functions are composable that way. But say you have a system behaviour that is a stream of function applications, e.g. [f(0), f(f(0)), f(f(f(0)))...] and I forgot the name for this function. This infinite stream is your system behaviour. Now we have a different behavio…

Co-inductive methods are useful for that sort of thing. For example, we can prove two infinite streams are equal by showing that their definitions/generators are "bisimilar".

But the question is not whether their infinite extensions or limit are equal, but whether at each finite combination some property about the stream progress holds.

Re: Why Specifications Don't Compose

#35

Post by hansvm »

sharkbot wrote: post #20

It would seem that the problem is the notion of composition is underspecified in this domain. My intuition would be that one needs a different mechanism of composition aside from the most obvious “use basic logic operators to combine two unrelated logic statements”. It’s unclear what “the composition of the two systems” really means. Are they running in parallel with no interaction (akin to two AWS instances in diffe…

I came here to say exactly this. The problem isn't that composing the two specs was hard, but that their desired "composition" required internal details from both specs.

The same difficulty arises in software development too. If the behavior you want isn't just a combination of other existing systems, but rather a combination which peeks inside and hacks on additional constraints then you're going to have a bad time. Maybe it's still worth it for some reason, but that's a leading indicator that a few files probably ought to be refactored.

Re: Why Specifications Don't Compose

#36

Post by Pet_Ant »

scotty79 wrote: post #25

All this is saying is you can't compose behaviors because we insist on having only one whole state, and only one concept of what 'next' state is. If you can have state with sub-states and 'next' operator that is respective to what sub-state we want to address then this example is easily composable. But then of course you might want to have substates interact with each other so it complicates further. It just looks li…

Sure but do you have formal model of such a system that is sound? I think unstated is that LTT is a known, intuitive, and well understood model. Sure you can ad hoc a fix but will it have any rigor?

Re: Why Specifications Don't Compose

#37

Post by simiones »

contravariant wrote: post #18
simiones wrote: post #13

Earlier quoted context omitted.

Not really, the problem described in the article could be rewritten to think of Next as a function World->World.

Though in that case requiring that Next blinks both 'x' and 'y' should obviously mean they are required to blink synchronously. Depending on how you model World you can either compose the two Next functions that blink x and y or you can multiply their respective worlds and use the product map. None of these feel unnatural.

Sure, that's a natural way of reading this requirement, but is it the right way? How would you specify the system such that it can produce:

[(x, y), (!x, y), (!x, !y), (x, !y), (!x, y), ...]

(that is, any interleaving of the two blinks that preserves the constraint that there is at least one blink in each "step")

Re: Why Specifications Don't Compose

#38

Post by gugagore »

kgwxd wrote: post #31
ahelwer wrote: post #24

Earlier quoted context omitted.

Can you describe how a formal specification system with namespacing would work?

Clojure Spec has it https://clojure.org/about/spec#_global_namespaced_names_are_...

To me Clojure Spec is more like IDL or a JSON Schema (or CBOR or Protobuf or etc), but with more "dynamic" stuff as opposed to just sum/product types.

It doesn't occupy the same space as, say, TLA+.

Re: Why Specifications Don't Compose

#39

Post by scotty79 »

Pet_Ant wrote: post #36
scotty79 wrote: post #25

All this is saying is you can't compose behaviors because we insist on having only one whole state, and only one concept of what 'next' state is. If you can have state with sub-states and 'next' operator that is respective to what sub-state we want to address then this example is easily composable. But then of course you might want to have substates interact with each other so it complicates further. It just looks li…

Sure but do you have formal model of such a system that is sound? I think unstated is that LTT is a known, intuitive, and well understood model. Sure you can ad hoc a fix but will it have any rigor?

That's the trade-off. Either you have things simple or expressive.

But I'm strong supporter of approach where you start with the semantics you want and work hard to make it work as opposed to simple to implement semantics you don't want because it makes programming harder.

I prefer TypeScript approach than C++ one.

Re: Why Specifications Don't Compose

#40

Post by tome »

If your programming language encourages you to structure your code in ways that don't compose when there are other perfectly good ways of structuring it that do compose then what you have on your hands is a bad programming language.
Post reply on HN