Ref: DTC/RBJ/011 Issue: 2/3 Date: 15th July 1986
This position paper presents an approach to the design and development of environments for the production of computer systems for which we require to have very high degrees of assurance of correctness.
The approach is shaped by particular concern for:
| a) | The soundness of the logical framework within which the correctness of the implementations is to be established, |
| b) | The inviolacy of the logical framework to errors on the part of the user. |
| c) | The means whereby the correctness of the implementation of the environment may be assured. |
In consequence the following characterise the approach proposed:
| i) | The approach is "foundational' rather than axiomatic. By this we mean that a single logical foundation is to be established during system design, and that users are permitted only definitional facilities which are guaranteed not to compromise the consistency of the foundation. |
| ii) | The foundation is supported by some philosophical examination of the nature of logical truth, and by careful examination of the intended domain of discourse (our "ontology") and the required expressiveness of the logic. |
| iii) | Both the foundation and its implementation are "reductionist". This means that the foundation is constructed from the simplest possible core, by the process of introducing new definitions, new syntactic forms, and exploiting (proven) derived rules of inference. The implementation is similarly to be built from a very small core in a carefully structured way. This reductionism is intended to provide maximal confidence in the consistency of our formal system, and the correctness of its implementation. We expect it to lead also to economies in implementation. |
| iv) | The foundation is type-free. A type system is to be constructed over the foundation for the purpose of providing transparent means of specifying the properties of the entities in the domain of discourse. These objects remain type-free, in the sense that self-application is permitted and polymorphic functions are "first class" entities, |
Our philosophical position has an intuitionistic flavour. We take the (absolute) truths of logic to be those statements which correctly express the consequences of applying correctly some effective procedure. We suppose the correctness of execution of the elementary steps of an effective procedure to be supportable only by an appeal to the intuition. This philosophical position provides some of the motivation for reducing our formal system to the smallest possible core. This ensures that our intuitions are relied upon no more than is inescapable.
Three levels of language are currently envisaged, each corresponding also to a system architecture, and a stage in development, The lowest level is illustrated by a formal system corresponding closely to pure combinatory logic. The middle level is intended to be an application independent type theory, The types in this system correspond to (partial) specifications and to recursively enumerable sets of terms which satisfy the specifications. At the third level are the prime languages for system development including abstract specification languages and implementation languages. Where possible specifications for implementations will be expressed in extensions to the programming language type system. The semantics of all these languages is ultimately expressed in terms of our primitive logical foundation, and hence the development is axiomatic only in the core foundation system.
0. CONTENTS
1. INTRODUCTION
2. PHILOSOPHY AND ONTOLOGY
2.1 Philosophical positions
2.2 Ontology
2.3 Logical Pluralism and Conventionalism
2.4 Neo-constructive Ontology
3. PRIMITIVE FORMALISATION
3.1 Introduction
3.2 Syntax
3.3 Axioms
3.4 Inference Rules
3.5 Abstraction
3.6 Definitions for encodings
3.7 Recursion
3.8 Decoding and partial encodings
3.9 Remarks on the Primitive Formalism
4. TYPES AND SPECIFICATIONS
4.1 Introduction
4.2 Recursive functions
4.3 Recursive sets
4.4 Recursively enumerable sets
4.5 Function spaces
4.6 Derived rules of inference
4.7 Types as values
5. APPLICATION LANGUAGES
6. IMPLEMENTATION
7. VERIFICATION
8. CONCLUSIONS
9. REFERENCES
©
dated 1986/7/15 HTML 1996/6/6 edited 1996/6/15