|
From: | Tim Daly |
Subject: | Re: [Axiom-developer] Proving Axiom Correct |
Date: | Tue, 3 Apr 2018 17:45:02 -0400 |
Dear All:
One of the main goals of program proof projects is to prove correctness of a piece of computer code. Given the myriad of computer languages, subject matters and their theories, algorithms, and implementation (which is not necessarily the same as the algorithm itself, since implementation requires choices in data representation whereas algorithms are more abstract), a proof system must limit its scope to be manageable, say for a particular language, a narrow subject matter, one of the theories, basic algorithms. It must then allow mappings of data representation to theoretical concepts/objects and verify compatibility of these mappings on inputs before proceeding to prove a certain implementation is correct. In certain situations (such as erratic inputs), error handling needs to be included. In addition, there are hardware-software interfaces (assemblers, compilers, instruction sets, computer architecture, microcodes, etc) that must have their own (program) proof systems.
So any claim that a certain program is "correct" can only be one small step in a long chain of program proofs. And if any change is made, whether to hardware or software in this chain, the whole program proof must be repeated from scratch (including the proof for the program prover itself). For example, a CPU or even a memory architecture change could have affected an otherwise proven program. Witness the recent Intel CPUs debacle in relation to a security flaw (due to hierarchical memory and prefetching on branches). Subsequent patches slow the CPUs, which would surely affect real-time applications, particularly those used for high-frequency trading: yes the program may still work "correctly", but does it really if a delay measured in microseconds causes a loss of millions of dollars?
Of course, proving any step in this long chain to be "correct" will be progress and will give more confidence to the computed results. Nonetheless, in the end, it is still always: "well-it-mostly-
works" . If a computation is mission critical, a real-world practitioner should always perform the same computation using at least two independent systems. But even when the two (or more) results agree, no one should claim that the programs used are "correct" in the absolute sense: they just appear to give consistent results for the problem and inputs at hand. For most purposes, particularly in academic circles, that is "good enough". If assurance of correctness is paramount, the results should be verified by manual computations or with assistance from other proven programs (verification is in general different from re-computation and often a lot simpler).
As a more concrete example, consider an implementation of an algorithm which claims to solve always correctly a quadratic equation in one variable: $a x^2 + b x + c = 0$ over any field (given $a, b, c$ in the field). The quadratic formula (in case $a \ne 0$) provides one algorithm, which can easily be proved mathematically, albeit less so by a computer program. However, the proof of the correctness of any implementation based on this formula is a totally different challenge. This is due to at least two problems. First is the problem of representation involving field elements and implementation of field operations. The second is that the roots may not lie in the field (error handling).
We may assume the implementation of the field operations are already proved "correct", but in implementing the quadratic equation solver, the programmer does not know much about the representation of the field (which is an input only known, partially, at run time). A correct implementation may need to distinguish whether the field is the rational numbers, the real numbers, complex numbers, the quotient field of an integral domain, an abstract field like an integral domain modulo a maximal prime ideal, a finitely generated field extension of another field, or an abstract field like the field of p-adic numbers. There would be little problem if the field is algebraically closed or is symbolic. What if the field is the field of real numbers, and the representation of a real number is a normalized floating point number? Such a representation would have problems like overflow and underflow not present in an abstract field. So, before we "prove" correctness, we need first to redefine the problem's scope, the algorithm, including input and output specifications, and if that is too general, we have to narrow the scope and implement different algorithms for different classes of inputs.
The point is, a general algorithm that can be proved (usually mathematically, or through pseudo-code using loop invariant methods if loops are involved) may still need to distinguish certain inputs (in the quadratic equation example, can the coefficients be 0? what type of field?) or else its implementation (also proved to correspond correctly to the quadratic formula) could still fail miserably (see Pat M. Sterbenz, Floating-point Computation, Prentice Hall, 1974, Section 9.3).
Questions that should be asked of any claim of proven implementation include: what are the specifications of the algorithm? is the algorithm (data) representation independent? how accurate are the specifications? How complete are they? A claim like "Groebner basis, is proven" (or Buchberger's algorithm is proven) probably has little to with proof of an implementation if it is done with "unreadable, consisting mostly of 'judgements' written in greek letters" (which I guess meant pure logical deductions based on mathematical assertions and computations involving some form of lambda-calculus).
Of course, for implementations, "well-they-
mostly-work" . That status will be with us for a very long time. While we should continue to work towards ideals (kudos to Tim), we must recognize that "good enough" is good enough for most users.
My ignorant and biased 2-cents.
William
William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031
homepage: wsit.ccny.cuny.edu
From: Axiom-developer <axiom-developer-bounces+wyscc=sci.ccny.cuny.edu@ nongnu.org > on behalf of Tim Daly <address@hidden>
Sent: Monday, April 2, 2018 1:37 PM
To: axiom-dev; Tim Daly
Subject: [Axiom-developer] Proving Axiom CorrectThere is the computer algebra field, where we spend mostand largely parallel efforts in computational mathematics.I've "discovered" that there are two large, independent,I've been working on proving Axiom correct for years now.
I've spent the last 18 months learning proof systems and
deep-diving into the theory (thanks, in part, to Carnegie
Mellon's Computer Science Department giving me the
"Visiting Scholar" appointment and faculty access).
of our time and effort. The concentration is on finding new
algorithms. This is interesting and quite satisfying. It appears
to be "progress". There is a large body of literature.
There is the program proof field, where a large number of
people spend most of their time and effort. The concentration
is on building systems to prove programs correct. On some
occasions a computer algebra algorithm, like Groebner basis,
is proven. There is a large body of literature.
Surprisingly though, there is little overlap. It is very rare to
find a paper that cites both Jenks (CA) and Nipkow (PP).
In fact, without a great deal of background, the papers in the
program proof field are unreadable, consisting mostly of
"judgements" written in greek letters. Or, coming from the
proof field, finding the computer algebra "algorithms" lacking
anything that resembles rigor, not to mention explanations.
Both fields are very large, very well developed, and have been
growing since the latter half of the last century.
It is important to bridge the gap between these two field.
It is unlikely that anyone will invest the millions of dollars and
thousands of hours necessary to "rebuild" an Axiom-sized
computer algebra system starting with a proof system. It is
also unlikely that anyone will succeed in proving most of
the existing computer algebra systems because of their
ad hoc, "well-it-mostly-works", method of development.
Axiom has the unique characteristic of being reasonably well
structured mathematically. It has many of the characteristics
found in proof-system idea like typeclasses (aka Axiom's
"Category-and-Domain" structures. What Axiom lacks is the
propositions from typeclass-like systems.
So the path forward to unite these fields is to develop the
propositional structure of Axiom and used these propositions
to prove the existing algorithms. Uniting these fields will bring
a large body of theory to computer algebra and a large body
of algorithms to a grounded body of logic.
Tim
[Prev in Thread] | Current Thread | [Next in Thread] |