4 ms·

I like to think of it as "application-as-functional-specification". A functional specification for a stateful system is a function from a list of all inputs to

by stevan 4y ago

I like to think of it as "application-as-functional-specification". A functional specification for a stateful system is a function from a list of all inputs to an output, i.e. `fun spec(inputs: List(Input)): Output`. This kind of specification doesn't need to specify `State` at all, as we can simply refer to previous inputs. E.g. imagine a counter system with the inputs `Increment`, `Reset`, and `Get`. The functional spec for `Get` is "find the latest reset and then count the number of `Increment`s since then". I think this is neat, because if you are developing the functional spec with a domain expert that doesn't know programming you don't wanna bother them with, for them, unnecessary bookkeeping details. From this spec you can then figure out what `State` needs to be, but this can be done as a separate step not involving the domain expert but rather other developers. I learnt this from the Cleanroom software engineering people, they call the spec without `State` a "black box spec", while the one with `State` is called a "state box spec". (There's also a third step called "clear box spec" where they break down the "state box spec" into functions.) I've been playing around with the idea of designing a specification language that lets you write "black box specs" together with some basic sanity checks of those specs, because I think there's a lot of value in this sort of structure. For example even if your application doesn't follow the "application-as-function" pattern, you can still use your "state box spec" as an oracle when doing property-based testing of your application.

iddan 4y ago
That idea sounds great. I think this kind of things really work well only in a dedicated DSL
- masklinn 4y ago
  It’s not that it works only in a dedicated DSL, it’s that if your language is too general it’s too easy to break out of the architecture when it’s a bother. So the pattern works, but you have to be religious about it, any breach will bring the entire thing down. Hence much easier if the language itself precludes breaking out of the pattern.
kodroid 4y ago
Hey, thanks for the input. > This kind of specification doesn't need to specify `State` at all, as we can simply refer to previous inputs. E.g. imagine a counter system with the inputs `Increment`, `Reset`, and `Get`. The functional spec for `Get` is "find the latest reset and then count the number of `Increment`s since then". I could be misunderstanding you, but this does not sound functional to me as `spec` seems to have access to previous inputs to `spec` invocations. What am I missing here? > I think this is neat, because if you are developing the functional spec with a domain expert that doesn't know programming you don't wanna bother them with, for them, unnecessary bookkeeping details. This sounds very similar to DDD (like as described as the DDD book at the end of the blog post). > I learnt this from the Cleanroom software engineering people At IBM direct, or are there any particular resources you can point to which you found useful? Many thanks for the contribution.
- nine_k 4y ago
  I suppose one should see "access to previous invocations" as function composition. The counter's description is literally Church numbers.
- stevan 4y ago
  > I could be misunderstanding you, but this does not sound functional to me as `spec` seems to have access to previous inputs to `spec` invocations. What am I missing here? In a stateful system (where outputs depend on previous inputs) you need to have access to all previous inputs in order to determine the output of some input, right? Also keep in mind that this is a specification, not an efficient implementation. If you'd implement it like this you'd have to recompute the output based on the inputs over and over again for each new input. And yeah, you can think of it as some kind of functional composition as nine_k pointed out. > This sounds very similar to DDD (like as described as the DDD book at the end of the blog post). Yeah, I think DDD gets this right: some lightweight methods (e.g. event storming) around inputs and outputs. But yeah, Cleanroom did this in the 80s. > At IBM direct, or are there any particular resources you can point to which you found useful? On this particular topic, see Harlan Mills' "Stepwise Refinement and Verification in Box-Structured Systems" (1988): https://trace.tennessee.edu/utk_harlan/16/ https://trace.tennessee.edu/utk_harlan/16/

by stevan 4y ago

iddan 4y ago

That idea sounds great. I think this kind of things really work well only in a dedicated DSL

masklinn 4y ago
It’s not that it works only in a dedicated DSL, it’s that if your language is too general it’s too easy to break out of the architecture when it’s a bother. So the pattern works, but you have to be religious about it, any breach will bring the entire thing down. Hence much easier if the language itself precludes breaking out of the pattern.

kodroid 4y ago

Hey, thanks for the input. > This kind of specification doesn't need to specify `State` at all, as we can simply refer to previous inputs. E.g. imagine a counter system with the inputs `Increment`, `Reset`, and `Get`. The functional spec for `Get` is "find the latest reset and then count the number of `Increment`s since then". I could be misunderstanding you, but this does not sound functional to me as `spec` seems to have access to previous inputs to `spec` invocations. What am I missing here? > I think this is neat, because if you are developing the functional spec with a domain expert that doesn't know programming you don't wanna bother them with, for them, unnecessary bookkeeping details. This sounds very similar to DDD (like as described as the DDD book at the end of the blog post). > I learnt this from the Cleanroom software engineering people At IBM direct, or are there any particular resources you can point to which you found useful? Many thanks for the contribution.

nine_k 4y ago
I suppose one should see "access to previous invocations" as function composition. The counter's description is literally Church numbers.
stevan 4y ago
> I could be misunderstanding you, but this does not sound functional to me as `spec` seems to have access to previous inputs to `spec` invocations. What am I missing here? In a stateful system (where outputs depend on previous inputs) you need to have access to all previous inputs in order to determine the output of some input, right? Also keep in mind that this is a specification, not an efficient implementation. If you'd implement it like this you'd have to recompute the output based on the inputs over and over again for each new input. And yeah, you can think of it as some kind of functional composition as nine_k pointed out. > This sounds very similar to DDD (like as described as the DDD book at the end of the blog post). Yeah, I think DDD gets this right: some lightweight methods (e.g. event storming) around inputs and outputs. But yeah, Cleanroom did this in the 80s. > At IBM direct, or are there any particular resources you can point to which you found useful? On this particular topic, see Harlan Mills' "Stepwise Refinement and Verification in Box-Structured Systems" (1988): https://trace.tennessee.edu/utk_harlan/16/ https://trace.tennessee.edu/utk_harlan/16/