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

21–30 of 65 posts

Re: Why Specifications Don't Compose

#21

Post by nonameiguess »

dejj wrote: post #3
veltas wrote: post #2

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

File types have specifications and at least some of them can compose. One of the more bizarre things I ever had to do for work was make a general purpose file comparison tool that could ignore certain classes of differences that were expected in order to validate program outputs against regression test keys. In one cases, xml files had base64 encoded pngs embedded in them, and the pngs had metadata chunks with xml embedded.

Another interesting case is the NGA is required to keep an archive of every geointelligence product created in the US for X years and the library only supports the nitf file format. This format specifies that images are stored as block segments that can either compose as tiles or as overlays, or in some cases can be non-viewable pixel data (i.e. something that can be used for downstream machine processing but isn't meant to be meaningful to humans and if you loaded it into a viewer it would look like nothing - consider something like a map of dead pixels).

One consequence of this is that if you want to disseminate something more lightweight to your customers ordering imagery products, like a simple jpeg so they don't need nitf viewers to see them, we make the jpeg and embed it as a nitf image segment with metadata indicating an actual nitf viewing program should ignore it.

There are Python build tools that get around the fact that their config isn't compatible with toml out of the box by embedding into pyproject.toml by adding a key value pair where the key is "legacy-ini" and the value is a string enclosing the entire config ini for the other tool. Or take secrets in Kubernetes, which specify key value pairs where the value is always a base64 encoded string, allowing you to store anything at all as a secret, including another yaml file, even a Kubernetes manifest. We presently use this where I'm at to get the Anchore Enterprise license into the cluster, and the license is in yaml format. Base64 encoded yaml embedded into another yaml file.

Of course, none of this all that exotic. File types are just a subset of data types, and obviously types compose, both functionally and in terms of building compound types, including recursive types, from simple types. I think the real issue this guy is seeing is due to temporal logic introducing unique challenges, not that specifications in general don't compose. Specifications without temporality compose pretty easily in many cases. This is why regular expressions and context free grammars and compilers are possible.

Nonetheless, the same issue would come up here. Given we can specify programming languages as context free grammars and regular expressions, why can't we compose them and have a compiler that compiles both Rust and Go at the same time and makes a single executable?

The answer is we can, but the syntax doesn't actually fully specify the languages. A full specification needs to include the runtime and the ABI, and the actual behavior of those may not be fully specified in any actual specification other than the code for the respective compilers. It's not that they can't be composed. SWIG is a thing. It's just much harder than composing CFGs. You probably can't do it in a blog post or by hand on a piece of paper.

Re: Why Specifications Don't Compose

#22

Post by BenoitEssiambre »

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.

Re: Why Specifications Don't Compose

#23

Post by marcosdumay »

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?

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.

Re: Why Specifications Don't Compose

#24

Post by ahelwer »

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?

Re: Why Specifications Don't Compose

#25

Post by scotty79 »

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.

Re: Why Specifications Don't Compose

#26

Post by Garlef »

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).

Re: Why Specifications Don't Compose

#27

Post by bqmjjx0kac »

maweki wrote: post #11
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?

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…

> and I forgot the name for this function.

I believe this is called `iterate` in Haskell.

Re: Why Specifications Don't Compose

#28

Post by dan-robertson »

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…

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).

Re: Why Specifications Don't Compose

#29

Post by dan-robertson »

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.

Re: Why Specifications Don't Compose

#30

Post by mmaroti »

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
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!

Post reply on HN