For relating programs and specifications there are two basic semantic approaches. By considering "programs as specifications" one defines a translation from a subset of specification expressions to programs. For example, equational specifications with axioms in the form of structural recursive definitions can be directly transformed into functional programs. In the type-theoretic approach it seems appropriate to consider programs as "realizers" of specifications, i.e. the semantics of a program is considered as a model of the specification.
More generally, type-theoretic descriptions are well-suited for integrating different styles of specifications and programs as has been shown by the DEVA project [Cazi 91].