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

41–50 of 65 posts

Re: Why Specifications Don't Compose

#41

Post by hwayne »

gugagore wrote: post #38
kgwxd wrote: post #31

Earlier quoted context omitted.

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

Clojure Spec is a contract system, which is a common way to write code specifications. You can formally verify it in theory; ACL2, another lisp, is used in formal verification. It's also hard to compose formally-verified code, as Lars talks about in the original link.

Re: Why Specifications Don't Compose

#42

Post by hwayne »

scotty79 wrote: post #39
Pet_Ant wrote: post #36

Earlier quoted context omitted.

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.

Then you've left the realm of formal specification of systems, though, so you're entirely outside the scope of the problem.

Re: Why Specifications Don't Compose

#43

Post by junon »

mmaroti wrote: post #30

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…

This. We use Hoare logic verification in software in very similar ways, to assert on symbol intervals to make sure arithmetic and memory operations can succeed in e.g. C.

Re: Why Specifications Don't Compose

#44

Post by gugagore »

hwayne wrote: post #41
gugagore wrote: post #38

Earlier quoted context omitted.

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

Clojure Spec is a contract system, which is a common way to write code specifications. You can formally verify it in theory; ACL2, another lisp, is used in formal verification. It's also hard to compose formally-verified code, as Lars talks about in the original link.

Thanks for the correction. I've wanted to see more examples of Clojure Spec in practice because I had really understood it as an interface description language.

Re: Why Specifications Don't Compose

#45

Post by scotty79 »

hwayne wrote: post #42
scotty79 wrote: post #39

Earlier quoted context omitted.

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.

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 those that come from pure mathematics.

Re: Why Specifications Don't Compose

#46

Post by hwayne »

scotty79 wrote: post #45
hwayne wrote: post #42

Earlier 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…

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.

Re: Why Specifications Don't Compose

#47

Post by skybrian »

jkhdigital wrote: post #8
MauranKilom wrote: post #4

Earlier quoted context omitted.

I read this as the "specifications" in "requirements and specifications" for e.g. software projects. For example, "there should be a button that pulls in new data when clicked". That's generally pretty different from formal/mathematical specifications.

I’d suggest that they are in fact the same thing, and differ only in the level of formality... somewhat akin to the difference between machine code and interpreted scripts.

An informal spec is about getting your intention across to humans who will interpret it in some reasonable way and fill in any gaps. It’s not math or a computer program at all.

David Chapman makes a distinction between rational and reasonable behavior, and it’s more like his “making breakfast” example:

https://metarationality.com/reasonableness-aspects

Re: Why Specifications Don't Compose

#48

Post by hwayne »

simiones wrote: post #32
neel_k wrote: post #15

Earlier quoted context omitted.

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…

If I'm being honest, a comment from /u/neel_k on this is enough to make me doubt my entire premise. He's a giant in the field and knows many, many things I don't.

Re: Why Specifications Don't Compose

#49

Post by [deleted] »

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?

[deleted]

Re: Why Specifications Don't Compose

#50

Post by scotty79 »

hwayne wrote: post #46
scotty79 wrote: post #45

Earlier quoted context omitted.

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…

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.
Post reply on HN