5. APPLICATION LANGUAGES
The expressiveness of our formal system is sufficient we believe to define the denotational semantics of application development languages. By providing a logically secure framework within which specialised type theories with matching derived inference rules may be established, we hope to enable a close fit between application languages and specification languages. This may enable a development methodology in which specifications are evolved into implementations by stages which are supported by automatic verification.