Sat Dec 7 12:41:36 EST 2019

Implementation / Specification codesign

So let's make this concrete by inventing an event + state machine
language that can be compared with an implementation, with maps going
from implementation to specification, but not backwards.

When there are backwards maps, great!  Those are modules for which
code generation can be used.  But this is _never_ guaranteed.

So a model-based approach should really take that structure: semantics
can always be assigned by projecting an implementation into model
space, and the reverse is optional but never guaranteed.