Machine Readable Specifications at Scale | Hacker News Reader

Machine Readable Specifications at Scale

alastairreid.github.io

37 pointsfanf216 comments

What I want to see is a specification language that can be compiled to natural language. This should be easier than trying to parse a natural language specification into something more machine readable. Standards documents are already quite often very stereotyped, so "compiling" to them seems like a good step. There would be a backup to insert unstructured (if perhaps parameterized) text, but it would have to be made somewhat awkward to discourage its use.

I think "natural language" is underspecified. E.g. it probably wouldn't be that hard to write some kind of templating engine that takes an XSL schema and outputs something resembling plain English. Except, the output would likely read like the most horrible legalese you can imagine.

Then you have some like the algorithmic definitions that proliferate most of the web platform/HTML5 specs. Those are all "cookbook style" lists of steps written in plain English - and it's easy to understand what an individual step does. However, understanding what the whole algorithm does - or even more, why it does what the spec says - is just as hard as it would be with code or pseudocode.

The reason I want this is not to make the standards easier for people to understand. Sure, the standards will be in legalese. But they are already in legalese. The goal is to make the standards more comprehensible to machines as well, without further degrading their (already problematic) comprehensibility to humans. Kill two birds with one stone.

Have a look at the WHATWG specs then - this might be a lot like what you want. E.g. Fetch [1].

Effectively, most of the spec could be written in pseudocode, except they expanded each pseudocode line into a complete sentence and annotated the whole thing with markers, links and commentary. The result is the afromentioned "cookbook style".

I'm not sure if this is actually easier to read than pseudocode though.

[1] https://fetch.spec.whatwg.org/#fetching

This is feeling like it has too much repetition. It might be better to compile that repetition to a table. Also, a compiler-to-natural-language should insert anaphora when appropriate.

One might also ask how one encodes motivational statements into a more formal spec. For example, what does it mean to say what the "purpose" of something is? Also, general specifications ("whenever you do X, also do Y") should be possible. Considerations like that are interesting even without the translation-to-NL aspect.

> One might also ask how one encodes motivational statements into a more formal spec.

Well, you can always add preambles or annotations that are not machine-readable.

If you really want to stay machine-readable, you could try to work with logical proposition languages, such as PROLOG. Also, I think goal trees (or goal DAGs) could be interesting. Something along the lines of "Our top-level is to help the user maintain invariant A. To archieve this, we implement features B, C, D. Feature B requires technical change E in service X while features C and D must be developed jointly and will require changes F and G in services X and Y..."

Of course something like this always looks vastly simpler than it actually is. I think in many cases, you'll be hard-pressed to even formulate a top-level goal in ordinary language. (Apart from the real goal: Someone from the C-Suite wants this feature)

The question also remains: What do you want to do with that machine-readable representation. The best representation will be strongly dependent on your use-cases - and formal languages without clear use-cases have a risk of devolving into cargo-cults and empty rituals. (See the whole navel-gazing around REST and HATEOAS)

There are many things one might do with such a representation. One that I am particularly interested in is connecting it to a program that implements the specification. That is, link the functions, variables, types, etc. of the program to corresponding parts of the spec. One could use this to generate documentation, traceability matrices, to generate unit tests for parts of the program, and to support evolution of the program as the specification changes.

TLA+ from MSFT Research is a formal specification language. See: https://lamport.azurewebsites.net/tla/tla.html

Leslie Lamport, the author, mentions some examples of industrial use of TLA+ at MSFT, Intel, Amazon and a few other orgs.

https://github.com/tlaplus/tlaplus

We have an internal JSON format for specifying the firewall configurations of all our servers. Essentially just "this group of servers can access this group of servers on these ports". Together with an idempotent "make it so" script, it has been a lifesaver.

> This is incredibly valuable because a good testsuite lets you check your specification.

Could the test suite actually serve as the specification?

Tests are specifications, but they can only encode "there exists" statements. For example, consider a test like this:

    def canUpdateUsername():
      u = User("u1", "user@example.com")
      n = "u2"
      assert u.setUsername(n).getUsername() == n

As a specification, this states that there exists a user 'u' and a username 'n', such that u.setUsername(n).getUsername() equals n.

We prove that statement by providing explicit examples of 'u' (the value User("u1", "user@example.com")) and 'n' (the value "u2"), and the computer checks the proof by executing the code. That execution is equivalent to substituting-in/inlining definitions, and rewriting primitives like 'if (True): x', until we get the value 'True'. QED.

Usually what we actually want is a "for all" statement. Sometimes tests can achieve this by being exhaustive, e.g. checking every boolean, or all 256 bytes. More generally, a "for all" statement is a function, e.g.

    def canUpdateUsernames(u: User, n: str):
      assert u.setUsername(n).getUsername() == n

This is a better specification, since we're asserting the relationship between 'setUsername' and 'getUsername' for any/every User and string. Unfortunately, we can't prove this by substituting-in/inlining definitions, since we don't have definitions for 'u' and 'n'.

One way to prove it is to use a more general approach, e.g. using equational rewriting, induction, etc. That's the approach taken by (interactive) theorem provers, but it can be a lot of work. Systems I've used for this include https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what... https://coq.inria.fr https://www.idris-lang.org and https://isabelle.in.tum.de

An easier alternative is to try disproving the statement, by executing it on thousands of examples and seeing if any fail. That gives us less confidence than a full proof, but can still be better than traditional "there exists" tests. This is called property checking or property-based testing. Systems I've used for this include https://hypothesis.works https://hackage.haskell.org/package/QuickCheck https://scalacheck.org and https://jsverify.github.io

Thank you for sharing your reply.

So what would such a language look like?

A 'table' scheme for syntactic forms which would be compiled to an FSM (equiv to a regular) language for processing. Assuming each row has a tuple value, any document definition language (such as JSON) would do as the front-end that spits out the RL.

https://en.wikipedia.org/wiki/Regular_language

I am a functional safety engineer for industrial plant and equipment and this exactly what I do for designing the sequencing and safety systems for large fired equipment. Either single FSM or a hierarchy of them when there is multiple burners.

I wrote myself a package using PyQt that sort of looks like a special spreadsheet that allows the combustion engineers to specify and also simulate the logic on a scan by scan basis.

The supporting logic "engine" is actually so simple as to be effectively 4 bitwise ops on bit packed words, per state (I use Mealy machines so the outputs are coupled directly and synchronously to states). Bonus is first up alarms and whats holding you out from next state all come for free in the logic used and you can derive a bunch of test cases automatically.

The sim/spec tool could export code ready to import to the controller, but we haven't had the economies of scale to support the required generalised tool testing this would require, but it does generate a bunch of hex codes that are the "configuration" that controls the functionality, interpreted by the 'engine'

A bunch of other bonuses, it allows you collect notes in a rich text doc behind every transition or condition cell and it can export these to make an easier to read human readable spec, it has an OPC server so you can couple it up to a HMI and do some basioc training or simulation demonstration, or you can bolt it onto an existing machine and see how well it "shadows" it if you are doign a retrofit or brownfields job.

The improved quality of outcomes and traceability etc (all the good engineering things desireable) yielded by an executable specification has increased by at least an order of magnitude by having a tool of this nature.

Previously most systems like this were effectively done by specifying with a "crappy narrative". This usually entailed, at best, a collection of vague thoughts about some things that were wanted, and some things that weren't, often some in conflict, and a not mentioning a bunch of negelected things. You then rolled the dice on the programmer and hoped they knew enough to ask the 3000 needed questions to somehow come up with adequately coded functionality. New tool is way, way better.

A final note, a joke I am sure most of you know, about why English is a poor specifying language and the sort of thing that drove me to take this path (with English it's all about assumed context)

   A wife asks her husband, a software engineer, "Could you please go shopping 
   for me and buy one carton of milk, and if they have eggs, get 6!"

   A short time later the husband comes back with 6 cartons of milk.

   The wife asks him, "Why the hell did you buy 6 cartons of milk?" 

   He replied, "They had eggs."

More interestingly: What would it mean? What is actually specified?

For instance, when I specify a messaging protocol I could use a FSM but would this implicitly assume that there is some form of "connection" between client and server that consists of a state in each of them.

So whenever I specify something, I need to start with a declaration of the entities and the list of possible events (and these events would carry data).

This way, the spec has an unintended effect on the implementation. Let's assume that I have some universal way to represent this data in all target languages (complicated but doable). If I then want to compile this FSM spec into test cases, I must offer some interface that mirrors the entities and events, essentially forcing me to explicitly program a FSM.

This is suboptimal because my implementation might not actually need this level of abstraction. A simple embedded C program might be described as a FSM but it could be implemented as a sequence of instructions.

Of course, we could also switch to integration testing, passing messages over sockets, etc. but then we would have to program the scaffolding around our mock client/server component and to benefit from the automatic test case generation we would have to either parse and interpret these automatic test cases or program our mock in a form that is defined by the specification output.

What I am trying to say is that there probably won't be a universal spec language. Instead, it should fit into the implementation eco system.

Reply on news.ycombinator.com