Designing a new language
Designers supply a list of properties that they wish to system to have
An axiomatic semantics is given defining the input language and how it achieves the desired properties
A denotational semantics is then defined to give a meaning for the language
A formal proof is constructed to show that the semantics contains the properties that the axiomatic semantics specifies
The denotational semantics is implemented using an operational definition.
Thus, these complimentary semantic definitions of a language support systematic design, development and implementation.