Sat Dec 7 12:33:46 EST 2019

Method: project model onto specification

So how to translate that into a method?

Does it make sense to implement the behavior at a higher level, to
then use it as a template?

Actually, very much yes.

It really seems that "adding" information to a specification to then
arrive at an implementation is the wrong way to look at it.

Work the other way around: "remove" information from an implementation
to end up with the specification.

This is textbook abstract interpretation.

It is very important to understand that an implementation in the first
place does _more_ than the specification.  Its substrate mapping has
many more observable effects than are necessary to implement the

It also might do _less_, in that certain corner cases are not handled.

The tragedy is that this is usually what people (me, really) focus on,
forgetting the part where an implementation is actually strictly
_larger_ than a specification.

This also makes it obvious that generating an implementation isn't
always possible.  There might be simply too many degrees of freedom
that really do not compose in a nice way.

I.e. changing a dataflow program into a sequential or pipelined
program introduces a very practically significant shift in timing
characteristics.  Something the specification might not care about at