up

7. VERIFICATION

There are well known and serious problems in verifying verification systems.

As a result of Gödel's work [Göd31], we know that a formal foundation system cannot usefully be used to verify itself. We are therefore bound ultimately to accept a formal foundation system which has not itself been formally verified.

Our reductionist approach to foundations is intended in part as a rational response to this situation, We suggest-that confidence in our ultimate formal foundations will be maximised in the following ways:

  1. The formal system should be as simple as possible.
  2. The system should be transparent to our intuitions.
  3. Essentially the same foundation should be subjected to theoretical scrutiny and practical exposure over a long period of time.

Our confidence in the consistency of first order axiomatisations of set theory is largely based upon their having survived over a long period of time without having been found inconsistent. We believe that the approach to foundations outlined in this paper satisfied points 1 and 2. We believe also that our formalism is sufficiently flexible to underpin a wide variety of more specialised formal systems and that this will increase its chances of receiving the exposure that will in due time contribute to confidence in its sufficiency and consistency. In fact we are essentially formalising recursive function theory, a subject which has now had some 50 years of scrutiny.

Our foundational reductionist approach results in the step from one logical level of the system to the next being achieved by definition rather than axiomatisation. This converts problems of consistency into logically less severe problems of opacity. This way of building on foundations is guaranteed not to compromise the consistency of the system, but if there are errors in the definitions then the concepts defined will not be the ones intended.

The implementation will be constructed in an analogous way. We therefore expect to implement the core foundation system as a logically secure bootstrap. This results in subsequent levels of development being logically guaranteed not to compromise the consistency or correctness of the implementation.

Implementation of higher levels of the system will also be provably correct against their specifications, but this only begins to be helpful once we have established specification languages which are significantly more perspicuous than our implementation languages.


up home © RBJ dated 86/7/15 HTML 96/6/6 edited 96/6/15