THE CONCEPT OF PROOF IN THE CONTEXT OF A TYPE-THEORETIC APPROACH, I: PROOF OF COMPUTER PROGRAM CORRECTNESS

When considering the concept of proof in the context of a type-theoretic approach, one should refer to the concepts of (1) proof of a computer program correctness, (2) proof of mathematical results by means of special computer tools, (3) proof from the point of view of the modern type-theoretical approach within the framework of univalent foundations of mathematics. This paper is devoted to the concept of proof of computer program correctness. Currently, computing devices surround us almost everywhere and are found in virtually every human activity. We are all interested in the correct functioning of our computers, so errors occur as rarely as possible, and at best do not occur at all. A formal proof using type inference gives certainty, provided that the formal system used in the proof is consistent and correctly implemented as a programming language. One of the purposes for which proof is formulated is to increase the degree of confidence. However, the proof itself does not give any conviction. If our belief in a proof is belief in the existence of pure formal proof, then the nature of mathematics is radically different from the nature of other sciences. If our belief implies a certain proportion of probability, then mathematics turns out to be similar to the natural sciences. The proof of the mathematical result is a "message", and not some ideal object. The social aspect of mathematical results greatly enhances conviction. In fact, it leads to the stabilization of key concepts, after which the result becomes part of recognized mathematical knowledge, and conviction in it may be sufficient to belief in the existence of purely formal proof. Proof of the computer program correctness does not have this characteristic. Further, it is assumed that the execution of the program leads to a change in the physical state of a particular computer. Since we cannot have a priori proofs for the a posteriori phenomenon, a number of researchers suggest that the concept of proof of correctness is a categorical error. Nevertheless, it is necessary to take into account the peculiarities of the concepts of abstraction and information hiding in computer science. With a careful approach, the concept of proof of correctness is quite reasonable and does not contain a categorical error.