This paper proposes an approach to the problem of building support environments for the development of very highly assured software. It does so, not from a pragmatic viewpoint, but from an idealist one. It represents an attempt to promote the convergence of computer science with constructive mathematics.
The ideas presented here are by no means fully worked out. They are presented as a basis for a programme of work, with a view to obtaining some feedback on the merits of the proposals.
The first four sections present our approach to logical foundations, and suggest how the most elementary logical basis might be built up by stages into sophisticated high level specification and implementation languages.
The first stage is philosophical, and consists in adopting an attitude about the nature of the mathematics of computing systems. The most important and concrete result of this philosophical stage is an ontology - a statement identifying the entities which we take to be the subject matter of computer science and which will constitute the domain of discourse of the formal systems we develop. Included in this stage is clarification of what sort of statements we wish to be able to make about the objects in our domain of discourse.
Having identified our ontology, we next construct a minimal formal language. In this language we may make statements about objects in our domain of discourse, and we may undertake formal derivations which establish the truth of some of these statements, In order that we may be able to obtain the highest degree of assurance of the correctness of our development environment, and in particular that we should be able to assure ourselves of the consistency of our formal systems and the correctness of their implementations, primary objectives in chasing this first level of formalisation are generality and simplicity. It is intended to be easy to reason about rather than easy to reason in, and hence consists of the simplest possible sufficiently expressive formal system. This system is type-free,
The third stage is the establishement of a more usable formal language in which the properties of entities may be specified and proven. This is done by providing a new syntax for constructs expressible in the basic formal system, and by establishing derived inference rules which facilitate proofs. The language in which specifications are expressed may be regarded as a type theory, The types in this theory are however purely a means of expressing specif ications. They place no restrictions on term formation, and play no part in securing the consistency of the logic, The "types" express properties of terms. A term may have many properties, and hence many types, The objects in the domain of discourse might therefore better be described as polytypical than polymorphic.
The formal "type-theory" we propose to establish during the third phase is the mathematical foundation for a variety of (more or less problem oriented) development languages,, among which Ada might number. These languages are addressed during our fourth phase. Such languages would be established by specifying their syntax and providing a denotational semantics in the type-theory. Along with programming languages such as Ada, specialised specification languages would be established, together with appropriate libraries of derived inference techniques. The programmer is thereby provided with a formal language in which he may reason in as natural a way as possible about the properties of his programs,
In section 6 we give some indication of how we propose to implement a support environment for these languages. Our final section addresses the problem of verifying such an environment.