It seems to me that your specification language (formal logic?) sucks. If you can't specify parameters, then you can't compose. That's all you seem to be saying. You define the concept of states, but then you complain that you can't differentiate between timing of states between x and y. Well that's your own fault for not having a powerful enough definition of how states work. This has nothing to do with specifications at a fundamental level.
Why Specifications Don't Compose
51–60 of 65 posts
Re: Why Specifications Don't Compose
#52Earlier quoted context omitted.
I used LTL because it's simple enough to explain the core ideas without getting bogged down in affordances and details. It's purely a pedagogical choice, just like how nobody explains the halting problem in terms of Java. Switching to a different notation helps with some of the practical details, but doesn't remove the essential problems that arise in composing specs.
The sorce of the problem with composability in this post is that you don't have a concept of sub-states and 'partial next' operators.
Would you be willing to provide a full example, replicating the dependent spec?
Re: Why Specifications Don't Compose
#53This 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?
The fact that CompCert, seL4, and similar projects exist is proof that a large amount of composition is possible if you have enough time to spend on it. It’s true that you can’t compose arbitrary formalizations, but you can architect your formalizations to be composable. Functional or stateful matters less than the engineering work required.
Re: Why Specifications Don't Compose
#54It 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.…
> The problem isn't that composing the two specs was hard, but that their desired "composition" required internal details from both specs.
But there's nothing 'internal'.
In conventional programming we pretend details are internal, e.g. by storing database handles as private fields. But that database is out in the real world.
TLA+ needs to be able to tell you that you can reach a bad state from a particular interleaving of reads and writes to a supposedly internal variable.
Re: Why Specifications Don't Compose
#55Earlier quoted context omitted.
The sorce of the problem with composability in this post is that you don't have a concept of sub-states and 'partial next' operators.
Would you be willing to provide a full example, replicating the dependent spec?
I'm wondering if you could as part of the O operator list all the variables in consideration for the "next"-state asar as that operator is concerned.
like O[a,b,c]X in the next state which is determined by a change to any of a, b, or c, then X will be true. In the case where the set of variables is all of them they can be omitted and thus get the existing behaviour.
I also suspect that the O operator with with a subset of variables will behave identically to other instances with the same set.
However, I feel like this will still hit walls before practical limits, Beth would just need a non-trivial example
Re: Why Specifications Don't Compose
#56Earlier quoted context omitted.
Then you've left the realm of formal specification of systems, though, so you're entirely outside the scope of the problem.
No. I haven't left anything. I'm just saying that expecting that useful widespread formal specification language will be something as simple as LTT is wildly optimistic and you should expect that it will rather mirror and encompass the complexities and requirements of actual programming, like necessity of composability. And it will most likely be somewhere between practical but unsound specification languages and tho…
It must be sound or it's of no use. Reminds me of the Ultraviolet Catastrophe. They had a theory that gave them precise answers, they just happened to be blatantly wrong.
Re: Why Specifications Don't Compose
#57Earlier quoted context omitted.
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.…
> The problem isn't that composing the two specs was hard, but that their desired "composition" required internal details from both specs. But there's nothing 'internal'. In conventional programming we pretend details are internal, e.g. by storing database handles as private fields. But that database is out in the real world. TLA+ needs to be able to tell you that you can reach a bad state from a particular interleav…
My phrasing could probably have been better there. Do you have any ideas for improvements?
The salient detail is not that you (or at least the verifier) can't reach in and look at the internal bits, but that if your goal is re-use then almost by definition you want to be able to take a whole spec, class, function, ..., and drop it in a new environment without having to wrap it in too many shims and modifications.
Going back to the programming analogy, if the typical way a class was used was by picking and choosing half the private members to reflect over then that would strongly indicate it was a poor abstraction for the current use case. If you wanted to build a system using classes like that as your primitives then you'd incur a lot of development overhead from the impedance mismatch between the thing you want to build and the blocks you're trying to compose to build it with.
TLA+ is a little mathy right? Let's tackle the idea from a different perspective :) The idea behind composability as used by the author is that you want complex specs to be describable as simple functions of simple specs -- C = f(B, A) where f isn't too distasteful. We don't just see that idea in programming and formal models; famous math problems often have that flavor [0], and in general it's pretty common to want to know what you can build from a set of blocks or to design blocks that can build lots of things. The insight the author had is that some things aren't cleanly related in _that_ way even if as humans we can "intuitively" see _some_ kind of a connection.
Drawing a parallel to the real world, if you had two blinker systems (including power and other garbage) each adhering to some kind of blinker spec (always on or off and with some kind of guarantee that you'll keep alternating between those), you'd have a devil of a time composing those two blinkers to create a system of two blinkers which were in sync, whereas with a different set of building blocks it could be easy to create the desired result. The problem you uncovered isn't that the real world is hard to compose though, but that your chosen abstraction didn't fit the problem very well.
Re: Why Specifications Don't Compose
#58I 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…
I don’t understand this at all. Either you have a totally different definition of namespacing to me (For me, this is basically getting to write x in most places and Foo::x and Bar::x in some places instead of foo_x and bar_x everywhere), or you’re just not addressing any of the issues discussed in the article (fairness, liveness, framing, etc).
Look at the 2nd paragraph of the motivating conversation:
``` Lars, 7:53: In software engineering, we have largely figured out modularization. All modern programming languages have some form of module system. You can pull in a module and import its functions anywhere. ```
... and then they write a blog about how this is impossible.
namespace is one trivial part of modularization (avoiding naming clashes). All implementations of LTL I have used do not have it. There is no good reason.
Your mentioning 'fairness' and other concepts that are part of expressing proofs on top of a state evolution system. Yes, the proofs are why we are using LTL, BUT, a good amount of time is spent building the model we wish to prove stuff about. There is no reason the state transitions cannot be namespaced and modularised, and it would save a ton of time, even if we have to express proofs globally of the "tree of state space".
Even on the proof level though, liveliness is a property that demonstrates the system never gets cornered. I am pretty sure that for many systems that will be expressible in general terms for a wide family of interesting systems. So I am pretty sure their argument doesn't hold even at the proof of properties level.
The real reason is abstraction is not something the logicians will get cited on, so it's a waste of their time trying to solve that thankless task. And probably they would not be very good at it anyway.
Re: Why Specifications Don't Compose
#59I 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?
Something equivalent to hierarchical state machines.
Re: Why Specifications Don't Compose
#60Earlier quoted context omitted.
> The problem isn't that composing the two specs was hard, but that their desired "composition" required internal details from both specs. But there's nothing 'internal'. In conventional programming we pretend details are internal, e.g. by storing database handles as private fields. But that database is out in the real world. TLA+ needs to be able to tell you that you can reach a bad state from a particular interleav…
My phrasing could probably have been better there. Do you have any ideas for improvements? The salient detail is not that you (or at least the verifier) can't reach in and look at the internal bits, but that if your goal is re-use then almost by definition you want to be able to take a whole spec, class, function, ..., and drop it in a new environment without having to wrap it in too many shims and modifications. Goi…
Just thinking out loud, this feels a bit like the problem ML’s module system is meant to solve: allowing the specialization of modules without needing to uncover the internal details of the implementation. I wonder if some of the same machinery would apply in this case. One would likely need a typed linear temporal logic theory to make it work.