axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

## Re: [Axiom-developer] Proving Axiom Correct

 From: William Sit Subject: Re: [Axiom-developer] Proving Axiom Correct Date: Wed, 4 Apr 2018 22:03:49 +0000

 ​                                                                                                                                                           Dear Tim: Thanks for your reply. I acknowledge my ignorance (and bias) on most of the advances in program proving.  "Getting it to mostly work" is not mathematics. That is true, but "getting it to work always" must be mathematics and yet, even mathematics itself is not perfect: there are gaps in mathematical proofs that authors sometimes miss but can be fixed, and there are ones that cannot be fixed because the argument is simply wrong as shown by counter-examples. Proving a program correct, however, is more than mathematics alone, and however careful the theory of program proving and self-applied to its implementation to create a proven kernel, it is done by humans and humans make errors. Coq falls into this category: In computer science, Coq is an interactive theorem prover. It allows the _expression_ of mathematicalassertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an but includes automatic theorem proving tactics and various decision procedures. Seen as a programming language, Coq implements a dependently typed functional programming language,[3]while seen as a logical system, it implements a higher-order type theory. Coq appears to be suitable to prove formally specified algorithms (I could be wrong) in a strongly typed language like Axiom.  So any Axiom function may be given a formal specification in order to prove a particular implementation is correct.  Can you point me to documentation on how much of Axiom library has passed through Coq this way? I am particularly concerned about the bootstrap portion (where the dependency of types might be circular---you have worked hard on that, and how Coq helps). I suppose that is what Coq on Coq does, getting a proven kernel. Proven hardware, proven operating systems, proven compilers, and proven languages exist now. That depends on what the objectives and meaning of "proven": for what set of specifications was attached to an implementation (hardware or software) that was "proven"---not merely "verified".  While the theory behind CC may be formal mathematics, in practice, it seems to be a rewriting system with inference rules (for example the beta-reductions). My point is simply to distinguish the task for proving correctness of an implementation from the correctness of an algorithm or the (mathematical) theory behind the algorithm. The experts of course realize (or should have realized) that.  >>My website contains 6 years of work I did on defining the hardware semantics of the Intel instruction set. I admire your dogged tenacity. You have rightly limited your scope to the "Intel instruction set". Of course that means someone else should work (and I assume have worked) on other instruction sets (including those that emulate the Intel instruction set).   In my local version of Axiom, during the build phase, I run ACL2 and Coq to "re-prove" the code that has been proven. Proof checking is considerably easier than proof discovery. So, yes, the "program proof >>is repeated from scratch" during build. What do you mean by "proof checking"?  If I understand Coq, it (discovers and) produces a step by step logical sequence proving the specifications (including any alleged proof of theorems) are correct (and correctly implemented?). Are you referring to checking that sequence? That would be valid if the program under re-certification has not changed, but any change (even if just by renaming one variable, say due to a typo). would require a de novo program proof (throwing away the previously discovered sequence of proof that established correctness). I didn't say and I am not saying that working towards a more perfect and error-free program proving system is not important. Keep up the good work. I better stop until I learn more on the topic. 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: Tim Daly Sent: Tuesday, April 3, 2018 5:45 PM To: William Sit; axiom-dev; Tim Daly Subject: Re: [Axiom-developer] Proving Axiom Correct   William, That's an interesting reply. In general, I agree with the points you make. Some overall comments are in order. For the last 18 months I've been working with people at Carnegie Mellon in Computer Science. One thing that really stands out is that virtually all the courses have a strong emphasis, if not a complete focus, on type theory and program proof. The "next generation" is being taught this from day 1. People like me are WAY behind the curve. Another comment is there is a HUGE literature on program proof which I was mostly unaware of. There is great progress being made, both in the theory and in the practice. >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. I have been researching the issue of "proving down to the metal". I have become aware of a lot of work in this area. Proven hardware, proven oprating systems, proven compilers, and proven languages exist now. For Axiom I've been concentrating on two levels. I'm using ACL2 for the Lisp code and Coq for the Spad code. My website contains 6 years of work I did on defining the hardware semantics of the Intel instruction set. See >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).  In my local version of Axiom, during the build phase, I run ACL2 and Coq to "re-prove" the code that has been proven. Proof checking is considerably easier than proof discovery. So, yes, the "program proof is repeated from scratch" during build. >Of course, proving any step in this long chain to be "correct" will be >progress and will give more confidence to the computed results. Agreed. >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) Clearly you're unaware of the notion of a proven kernel. See Barras and Werner "Coq in Coq" which goes into much greater detail than is appropriate here. Verifying algorithms, e.g. the GCD, has been done since around 1968. The world has gotten much better in the last 50 years. At the bleeding edge, Homotopy Type Theory has things like a theory of coercion which may end up being part of the Axiom proof pile. >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). You're well aware of the Category structure of Axiom. Consider that each proposition is attached at the appropriate place in the Category hierarchy. Propositions are also attached to Domains. Proving the GCD in the Domain NNI is different from proving the GCD in any of the other Domains. You inherit different propositions and have local propositions appropriate to the chosen domain. The representation of elements of these domains differ and they are available during proofs. As for the issue of error handling, what you identify is an error that is generic to the problem domain, not an error in the implementation of the algorithm. These are different classes of errors. >...[elide]... >A correct implementation may need to distinguish whether the field is >the rational numbers, the real numbers,  complex numbers,  ... This is the beauty of Axiom's structure. There are different algorithms for different domains, each having different propositions that carry the assumptions relevant to that Domain and the particular algorithm, as well as any that are Categorically available. >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). See Gustafson, "The End of Error" and his online debate with Kahan. >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? All good questions. What is the specification of a sort? It not only must state that the results are ordered but also that the result is a permutation of the input. Axiom has the advanage that a portion of its algorithms have mathematical specifications (e.g. Sine, GCD, etc.). Furthermore, additional properties can be proven (gcd(x,y)=gcd(y,x)) and used by the algebra at a later time. >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). Start with Martin-Lof and Gentzen. I can't begin to generate a response to this because it's taken me 18 months to get up to speed. Without an intense study of the subject we have no common ground for understanding. I'm not trying to dismiss your claim. It is perfectly valid. But there has been 50 years of work on the program proof side of mathematics and without a deeper understanding of that work it is hard to communicate precisely. It would be like trying to explain Computer Algebra's ability to do Integration without mentioning Risch. >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. Yeah, they "mostly work", except when they don't. Distinguish hacking from mathematics. "Getting it to mostly work" is not mathematics. Which is fine, if that's all that matters to you. I agreed that hacking is "good enough for most users". That said, this effort is research. It is an attempt to unite two areas of computational mathematics, both with 50 years of rich history. Most users don't care. In fact, no one cares but me. Which is fine. I fully expect to publish a series of minor papers no one will ever read. And, given the magnitude of the task, I am certain it cannot be completed. In fact, I devote a whole chapter of Volume 13 to "Why this effort will not succeed". To quote Richard Hamming: "If what you are working on is not important, why are you working on it?" I think this research is important. Tim On Tue, Apr 3, 2018 at 1:11 PM, William Sit wrote: 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 on behalf of Tim Daly Sent: Monday, April 2, 2018 1:37 PM To: axiom-dev; Tim Daly Subject: [Axiom-developer] Proving Axiom Correct   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). I've "discovered" that there are two large, independent, and largely parallel efforts in computational mathematics. There is the computer algebra field, where we spend most 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

reply via email to

 [Prev in Thread] Current Thread [Next in Thread]