This is blatantly false. People are using formal verification tools in hardware design, and they do work and they do compose. Here is a simple verilog code which accomplishes some of what he wants.

  module Blinker (
   input wire clock,
   output reg state
  );
  
  always @(posedge clock)
   state <= !state;
  
  `if FORMAL
  
  always @(posedge clock)
   assert ($past(state) != state);
  
  `endif
  
  endmodule
  
  module testbench (
   input wire clock,
   output wire state1,
   output wire state2
  );
  
  Blinker blinker1(clock, state1);
  Blinker blinker2(clock, state2);
  
  `if FORMAL
  
  # assume that they are different
  assume (state1 != state2);
  
  # then they stay different
  always @(posedge clock)
    assert (state1 != state2);
  
  `endif
  
  endmodule

Of course you NEED clock wires to the blinker. Composability comes from the use of assume and assert. You assume that your environment is behaving according to spec and you prove that you are also behaving to spec PROVIDED the environment working correctly. See https://symbiyosys.readthedocs.io/en/latest/index.html for more details.

Moral of the story: broken spec cannot be used, and I am saying this as a mathematician!

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. Academics only apply it to toy problems, so it never needs the scaling features like namespacing.

Its not about logic. Thats just post-hoc stockholm syndrome.

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 different data centers running each program)? Are they running in parallel with superficial interaction (two threads in the same process)? Are they running concurrently with mediated interaction (coroutines)?

The nature of how the programs are composed necessarily would influence the nature of how the specs should be composed, I would think.

Finally, maybe the fault lies with the logic system, rather than the problem?

I wonder to what extent this is a problem from the global timesteps of LTL. They seem to require global transformations to work around and the result of the transformations seems to be harder to reason about. I wonder if some alternative logic would work better (eg one where time is more continuous and so there is no such thing as the X operator, or maybe one where time is partially ordered in some way but I’m not sure what that would look like).

I don’t really know how to talk about the problem of the shared variable coupling the two processes too tightly. It seems like the logic is too relaxed in allowing any variable to change at any time forcing specifications to lock down variables and therefore be too brittle to connect.

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 like multithreaded programming.

Ah, 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.

In practice, expressible specs are always, always, always incomplete. Some requirements just don't fit into any usable formalism. Some that do fit unavoidably overspecify behavior, so that, e.g. more efficient, acceptable behavior would be disqualified.

There are reasons why we don't just write formal specs and generate a system from them. It is not just stubbornness.

What is astonishing is that certain, isolated systems have been generated from formally complete specs. They need to recognized as miraculous, unique and unrepeatable.

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?

tl;dr:

"Here are some binary operators for a certain notion of specification and some very good examples of why these are not sufficient to express some obvious specs we would like to express."

But:

As others have noted: The given notion of composition is to restricted. The central shortcomming, as indicated in the article, seems to be that the individual parts need to be reintegrated into a new whole. Binary operators can obviously not do this.

Candidates for a compositional calculus that should be able to deal with this are operadic composition via wiring diagrams and comprehension expressions interpreted via arrows (here, the final return/yield is used to reintegrate the individual parts).

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.

Please change title to reflect that this is not about "specifications" in the more common usage and is about formal methods.

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.

This is interesting and in my opinion appropriately blurs the line between code and specs.

I don't know what the standard is nowadays but in the past, every time I have argued against a purely natural language specification in favor a code based spec such as a reference implementation, people looked at me in shock that I wanted to skip the specification part.

I tried to explain that, I don't want to skip the specification. I just don't think human language is nearly precise enough to write an adequate specification. Natural language words are incredibly polysemic and contextual. Look, for example, at how many meanings the word "break" has: https://www.merriam-webster.com/dictionary/break

Kolmogrov has a long time ago suggested that fully specified information distills down to computer programs: https://en.wikipedia.org/wiki/Kolmogorov_complexity, https://en.wikipedia.org/wiki/Minimum_description_length

To me the ideal language for a pure specification might be a mix of natural language and pseudo code with a pseudo test suit. However, if you are writing this, you might as well go one step further and write working testable code.

I like the concept of Literate Programming (https://en.wikipedia.org/wiki/Literate_programming) and its descendants like having code with extractable inline comments that auto generate documentation. I would argue that modern pull request based workflows that tie discussions to version controlled code changes are also the progression of this line of thought. A cleaned up version of these make sense to me for a specification.

And I get some of the concerns. While natural language under specifies, reference implementations over specify. This is more of a problem with low level languages. Modern high level languages are getting fairly close to a form of pseudo code. I fully agree that the reference implementations shouldn't contain or should hide, low level optimizations.

I also understand that reference implementations can unduly tie specs to specific hardware, OSs and platforms.

But to me over-specification is less of a problem than under-specification and it can be mitigated by labeling particular functions or blocks of code as implementation specific and not part of the spec.

Without spec written in code, the different implementations always have subtle incompatibilities. I see egregious versions of under specification in government where horrendously bad spec are created in order to issue RFPs for getting software built. They usually end up with non working software at mind blowing cost.

People have this weird misconception that you are contracting out to build software. You are not. Building software is really easy. You press the build button or type the compile command. Building software has been fully automated for a long time. What is difficult is designing software and specifying what it must do. This is because there is a vast jungle of protocols, business flows, hardware and software platforms that need to be interacted with differently for different needs. This is what needs to be specified and only computer code can do it adequately.

I really wish, for example, that Mozilla adopted the chromium core. To me chromium is a de facto standard spec. I don't think it is possible to specify a standard that makes browser fully compatible without them having a common core based on a reference implementation. And we really need a popular non-profit managed release of said reference browser core.

i also don't agree with this. specs are referenced by other specs all the time.

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, specification composition (taken in the sense of the article, to mean the ability to state properties and proofs in a way which aligns with program module boundaries) has become a relatively routine technique in the last 5-10 years.

Basically, there are three main ingredients we seem to want: (1) you need to understand the abstract resources your program manipulates and how different parts of the program transfer ownership of these resources, (2) you need to understand the protocols (i.e., state machines) that your program components are participating, and (3) you need to understand the rely/guarantee invariants that the program components are maintaining.

Historically, verification techniques have had good stories for one or two of ownership/protocols/invariants (eg, TLA+ struggles with handling ownership), but the research community has developed techniques in the last few years that can handle all of them. As a result, there don't seem to be many small programs out of the reach of program verification -- compositional machine-checked proofs lock-free data structures over weak memory are a thing people can do these days. These proofs are by no means easy, but that's because the algorithms are fundamentally intricate rather than because our proof techniques suck.

We don't have any kind of proof that this is a complete inventory of the techniques we need to verify these kinds of programs. But there is the empirical fact that there are fewer and fewer small programs we don't know how to verify, so it's not an unthinkable possibility.

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 behaviour [g(0), g(g(0)), g(g(g(0)))...]

You can (more or less) easily reason about the relation of g^n(0) to f^n(0) where both streams or behaviours are synchronous. But reasoning about the behaviour of all g^n(0) in relation to all f^m(0) is difficult.

All the useful properties for these streams, liveness, fairness, as well as other invariants, are not easily encoded.

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.

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

What the article calls specifications are exactly programs in a logical paradigm (not exactly FP, but you can translate into it).

My understanding is that the problem the article states is that in a synchronous system with a global clock, everything has to be synchronized to that clock. And that if you do not add cycle-number dependent logic, you can not have cycle-number dependent memory. I fail to see what it new there, or even non-obvious enough to warrant an article.

Hillel, you called me out on Twitter so I felt like it would be best if I elaborated for a few reasons. Firstly, hopefully it will be reassuring to know that although my comment seemed glib I was actually trying to engage with the substance of your work, secondly, it will help clarify my thoughts, and thirdly, someone else may be interested.

I don't have any experience with machine-verified specifications but I do have experience writing computer programs and (traditional, human-checked) mathematical proofs, so my comment comes from that perspective.

Regarding

> Me: 200 words on how we're talking about composing specifications, not code, because specifications aren't programming languages

> HN: [parent]

I'm sorry if the use of the terminology "programming language" was jarring. I tend to take the point of view that a huge range of human activity in what are traditionally called programming languages, probabilistic graphical models, languages for constraint solving and optimisation, a lot of mathematics (especially category-heavy mathematics) and even writing YAML for configuration is actually all just different aspects of the same thing. I chose the word "programming" in the parent which might betray some bias on my part but regardless of the word chosen the practice of combining smaller logical pieces into larger logical pieces is common to all. Your article is suggesting that there is something about the nature of specifications that makes this composition harder than it is for executable code.

The conclusion may be true (I have no idea) but I'm afraid that I just don't see how your article justifies it. In the first example I see a language LTL whose design encourages users to write small logical units that cannot be composed[1] easily with the && operation. A more awkward encoding does achieve compositionality (through stuttering-invariance). It looks like TLA+ provides notation to make it more natural to write the small logical units in ways that they can be composed easily with &&. That makes it sound to me like TLA+ is a better language than LTL (for this purpose)! Better languages make it easier and more natural to write smaller units in ways that can be composed. That's all my parent comment says!

In the second example it is composition with && itself that proves to be impossible. The composition rule is something more complicated:

    Next = (NextX(z) && Same(y)) || (NextY(z) && Same(x))
    Spec = InitX && InitY && □[Next]_xyz

Unless I'm missing something, there's nothing wrong or hard about that composition rule, it's just the tooling that doesn't make it easy to work with. In Haskell we compose monadic functions with >>=. That would make life really awkward unless we had do notation. The problem is not that monadic functions are hard to compose, it's that the language needs to support them ergonomically. I can't see anything in your post that suggests to me that specifications are by nature hard to compose. All I can see is unergonomic languages.

See also https://www.haskellforall.com/2016/04/worst-practices-should...

[1] composed in the sense which your article elaborates, that is, in a way which combines the properties of both in some desirable way

Not really, the problem described in the article applies to any kind of spec.

You could take the specs to be "x must blink" and "y must blink". Either of these informal specs are more or less explicit enough to implement directly, but the spec "both x and y must blink" can be interpreted in too many ways to implement.

What is the “more common usage” of the word “specifications”, for example?