Sun Jun 12 15:22:28 CEST 2011

Programs and specifications


The trouble is that representation needs to be as abstract as
possible.  This seems to be the hard part as very often it remains
implicit.  I.e. programmer thinks "Ah, let's use this bit for that to
quickly hack around doing these things separately".  That's exactly
the implementation information that one wants to capture, and has an
incredibly large amount of detail if made explicit.

This then also indicates why this process is not factored in the
following particular way:

   specification S . specializer (S->I) = implementation (I)

but by writing the implementation I separately, and providing a proof
that I embeds S.

Q: What is more difficult, to provide an indirect proof that S is
   isomorphic to a subpart of I, or to construct a direct
   (parameterizable?) embedding function S->I?

Putting it like that it seems that the former is simpler, as it allows
the use of non-constructive proof techniques.  However, making the
S->I embedder parameterizable might give a whole family of
implementations that do not need separate proofs.