We provide a constructive and intensional interpretation for the specification language Z in a theory of operations and kinds T. The motivation is to facilitate the development of an integrated approach to program construction. We illustrate the new foundations for Z with examples.