These arise from the rapidly rising cost and complexity of organisation and information in products, by constrast with the falling cost of the physical components from which a product may be manufactured.
This paper examines some of these new pressures, identifies some of the weaknesses which they highlight, and considers new approaches to foundations which they suggest.
0. CONTENTS 1. INTRODUCTION 2. SOME PROBLEMS IN COMPUTING 2.1 Some Objectives 2.1.1 Denotational Semantics 2.1.2 Formal Verification 2.1.3 The Mechanisation of Mathematics 2.1.4 Types as Specifications 2.2 The need for Self Application 2.2.l Operating Systems 2.2.2 Artificial Intelligence 2.2.3 "polymorphism" 2.3 Problems with Polymorphism 2.3.1 "Persistence" 2.3.2 Parameterisation of Specifications 2.3.3 Abstraction 2.3.4 Type Inheritance 2.3.5 Modularity 2.4 Some approaches to solutions 2.4.1 Scott Domains 2.4.2 Cardellils type:type 2.5 What we need in our foundations 2.5.1 A Universe containing the Universe 2.5.2 A type of types 3. ABSOLUTE AND NECESSARY TRUTH 8. CONCLUSIONS 9. REFERENCES1. INTRODUCTION
This paper presents at greater length ideas on Logic and the foundations of Mathematics first approached in my paper "Logical foundations and formal verifications".
It was not my intention in that paper to seriously address any philosophical issues, but the formal system which formed the main subject of the paper could not be justified as a foundation system without an appeal to philosophical ideas which had guided me to it. I therefore included in the paper those minimal philosophical preliminaries which I thought necessary to reveal the rationale behind the proposal.
2. SOME PROBLEMS IN COMPUTING
2.1 Some Objectives
The adequacy of any system must of course be measured against some purpose, and similarly a problem can only be appreciated if we understand what objective it inteferes with. Computing has now grown into a major international industry, most of which is not in the least concerned with mathematical foundations.
It is only when ambitious and far sighted ideals are considered that foundational issues can be argued to have any significance in
Computing. These ideas are inspired by two major long term ambitions, and will therefore be better understood if they are declared as background.
2.1.1 Computer Science and the mechanisation of Mathematics
Since the beginning of this century, notably exemplified by the publication of Principia Mathematica, it has been known to be possible in principle to derive all of mathematics from a small set of primitives using a fixed set of inference rules. Mathematicians have rarely shown any inclination to adopt this extremely of rigour in their demonstrations.
At least two obvious reasons can be cited for their laxity. Firstly, the length of fully formal derivations is much much greater than that of proofs normally found in the literature, and they contain much detail which is of no interest mathematically. So considerable penalties attach both for the author and his reader to the use of fully formal derivations. The only benefit hoped from such derivations is a greater degree of confidence in their correctness, but in his context it is unlikely to accrue. The presentation of a great deal of uninteresting detail in a proof to be checked manually is likely to decrease rather than increase the effectiveness of manual verification.
The availability of cheap powerful computer systems however, threatens to tip the balance. Given suitable software (and we do not claim that any existing software is suitable for routine use by mathematicians), the machine could complete all the tedium of detailed checking of formal proofs. We may eventually expect that they will supply sufficient assistance in the construction of such proofs that a fully formal proof can be constructed on a computer more easily than a less formal proof may be obtained without one. Furthermore, as computers are more frequently used by mathematicians, we can reasonably expect an increasing incidence of proofs being found using computers which could not have been found without them. A well known recent example (though not an example of machine generated or checked formal proof) is the use of computers in obtaining a proof of the four colour problem.
Complementary to this is an increased perception of the desirability of mathematically rigorous ways of developing software for computers. in connection with software development complexity is the greatest problem, Thus if proofs of correctness are to be economically obtained then maximal computer assistance will be necessary, and if large even though shallow proofs are to be reliably checked, this must also be done by computer. There is also a growing lobby claiming that for reasons of economics in the development of correct software an effective use of abstraction, enabling the maximal re-use of the mathematics of the problem domain, will be essential.
Thus it is suggested that by computing becoming more mathematical, and more abstract, it converges upon mathematics as it learns the better to exploit computers.
An ambition for the end of the century is to have developed the computer support for mathematicians to the point at which formal proofs can be more easily obtained with a computer than rigorour proofs without one. For the computer scientist the ambition is to sufficiently improve languages tools and techniques that programs will normally be specified in abstract specifications and then transformed until acceptable performance is obtained by measures which guarantee continued satisfaction of the specification., while supporting in addition the proof of additional properties not explicit in the specification. We conjecture that there is sufficient in common between these two ambitions that we may talk of the convergence of Computer Science with Constructive Mathematics, and hope for the effective computerisation of both.
2.1.1 Denotational Semantics
During the 70's considerable work was done on the semantics of programming languages. An important approach to this subject devloped at oxford by Scott and Strachey was that named "denotational semantics", This set a standard for defining semantics which included the following elements.
This standard of requiring a mathematical object to be available as the meaning of every independently meaningful syntactic object is one which can be carried to languages other than programming languages. It can be seen to be a desirable property of the languages within which mathematics in general is conducted. That this is not in general the case only fails to cause much greater concern than it evidently does, because mathematicians are not in general much concerned with whether their arguments can be formalised, or with whether they are readily reconstructable in one of the standard foundations.
2.1.2 Formal Verification
Software "engineering" has long been a cause for concern on two prime grounds. Firstly that the task of writing programs to enable computers to perform the tasks required of them is highly intensive in intellectual labour, and the shortage of sufficient skilled resource is a limiting factor on what can be achieved with modern computer systems. Secondly because of the very great difficulty in ensuring that computer programs fulfill their intended functions. Where a very high degree of assurance of the correctness of computer systems is required formal verification would seem to be desirable.
Formal verification of a computer system consists in obtaining machine
checked formal proofs that provided the components from which a system is build conform to their specifications, and the system is correctly constructed from these components according to a formally specified design, then the computer will satisfy its formally specified requirements.
There is some intended ambiguity here about what is a component, and what a design. This permits both hardware and software verification to be encompassed.
Two features of formal verification help to bring pressure on foundations.
Firstly the perception that for reasons of complexity a formal verification must be machine checked. This prevents solution of foundational problems by sleight of hand.
Secondly there is the fact that programs and their properties are the domain of discourse. This induces a desire to economise by bringing together programming language type system and logical type systems, and in turn this unification makes demains upon the type theory which cannot be met in classical systems.
2.1.3 The Mechanisation of Mathematics 2.1.4 Types as Specifications 2.1,5 Artificial Intelligence 2.2 The need for Self Application 2.2,1 operating Systems 2.2.2 Artificial Intelligence 2.2,3 wpolymorphism" 2.3 Problems with Polymorphism 2.3.1 "Persistence" 2,3.2 Parameterisation of Specifications 2.3.3 Abstraction 2.3,4 Type Inheritance 2.3,5 Modularity 2,4 Some approaches to solutions 2.4.1 Scott Domains 2.4.2 Cardelli,s type:type 2.5 What we need in our foundations 2.5.1 A Universe containing the Universe 2.5.2 A Type of TypesWANTED :
GOOD FOUNDATIONS with Type:Type
NEED: Specification Languages supporting formal reasoning which are closely integrated with programming languages.
SUGGESTS: enrich type system to enable types to serve as specifications,
BUT.. programming languages need type:type