We have outlined an approach to logical foundations for the formal development of computer systems which we believe when fully developed will offer:
|a)||The highest possible levels of assurance of the correctness of systems developed.|
|b)||High levels of flexibility.|
|c)||Economy of implementation.|
This foundation offers a particular advantage in the exploitation of abstraction, increasingly seen as an important tool for formal development. We offer a foundation within which mathematical concepts, without qualifications relating to cardinality, have denotations.
Considerable further work is necessary before we can be wholly confident that this approach can be made to deliver what we believe it to offer. It is inherent in our approach that once the definition of the formal systems has been carried through in a fully formal way, an inefficient implementation will be obtainable at trivial cost. Provided sufficient care is taken in design, we believe that tolerably efficient implementations will then be relatively inexpensive.