Proving Axiom Correct

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
13 messages Options
Reply | Threaded
Open this post in threaded view
|

Proving Axiom Correct

Tim Daly
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




_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Martin Baker-3
Tim,

I've been experimenting with a language called 'Idris'. I've been
playing around with writing some of the Axiom SPAD library code in
Idris. My code so far is here:
https://github.com/martinbaker/Idris-dev/tree/algebra/libs/algebra
Nothing usable yet, I'm just experimenting with whats involved.

So in the same way that Coq is a proof assistant which can generate some
code by Curry-Howard then Idris reverses that and starts with the
algebra code and allows that to be linked to proofs (which are types).

Idris is based on Haskell but with 2 very important differences which
make it very compatible with SPAD:
* It has full dependent types built into the language from the start.
(not a plugin like Haskell)
* It is eager, not lazy, by default.

Of course the language is pure functional so translating imperative code
is hard but its an approach that interests me, I would be interested to
hear what you think.

Martin

On 02/04/18 18:37, Tim Daly wrote:

> 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
>
>
>
>
>
> _______________________________________________
> Axiom-developer mailing list
> [hidden email]
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Tim Daly
In reply to this post by Tim Daly
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
http://daly.axiom-developer.org/intel.pdf


>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 <[hidden email]> 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

From: Axiom-developer <axiom-developer-bounces+wyscc=[hidden email]> on behalf of Tim Daly <[hidden email]>
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





_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

William Sit-3

​                                                                                                                                                           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 scienceCoq 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 automated theorem prover 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 provenProof 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 <[hidden email]>
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
http://daly.axiom-developer.org/intel.pdf


>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 <[hidden email]> 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

From: Axiom-developer <axiom-developer-bounces+wyscc=[hidden email]> on behalf of Tim Daly <[hidden email]>
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





_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Tim Daly
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

William Sit-3

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

www-inst.eecs.berkeley.edu/~cs150/fa05/Lectures/07-SeqLogicIIIx2.pdf
<a class="GHDvEf ab_button" href="https://www.google.com/search?client=safari&amp;rls=en&amp;q=Mealy/Moore&#43;state&#43;machines&amp;ie=UTF-8&amp;oe=UTF-8#" id="am-b5" aria-label="Result details" aria-expanded="false" aria-haspopup="true" role="button" jsaction="m.tdd;keydown:m.hbke;keypress:m.mskpe" data-ved="0ahUKEwje_6z3w6TaAhXwUN8KHQi5BeUQ7B0IXDAF" style="border-top-left-radius: 0px; border-top-right-radius: 0px; border-bottom-right-radius: 0px; border-bottom-left-radius: 0px; cursor: default; font-size: 11px; font-weight: bold; height: 12px; line-height: 27px; margin: 1px 0px 2px; min-width: 0px; padding: 0px; text-align: center; transition: none; -webkit-user-select: none; background-color: white; background-image: none; border: 0px; color: rgb(128, 128, 128); box-shadow: 0px 0px 0px 0px; filter: none; width: 13px; text-decoration: none; display: inline-block;">
and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

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: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  


_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Tim Daly
One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion.

I've spent a lot of time and study in the subject of understanding
better and less error-prone ways of programming. That has led me
to applying mathematics (ala Floyd/Hoare/Dijkstra). Given that
Axiom is about computational mathematics there is a natural goal of
trying to make Axiom better and less error-prone.

Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers.

My point of view is that writing Spad code that way is "pre-proof,
19th century 'hand-waving' mathematics". We can do better.

You obviously believe this is a waste of time. You are probably right.
But I've only got a few years left to waste and this seems to me to be
an important thing on which to waste them.

Tim


On Fri, Apr 6, 2018 at 1:23 AM, William Sit <[hidden email]> wrote:

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

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: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  



_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

William Sit-3

Dear Tim:


I never said, nor implied you are wasting your time. 


If there is any difference (and similarity) between our views, it is about trust. You do not trust Axiom code but you trust theorem-proving while I prefer to trust Axiom code and not so much on theorem-proving. Both research areas are mathematically based. Clearly, no one can in a life time understand all the mathematics behind these theories, and honestly, the theories in theorem-proving (including rewriting systems, type-theory, lambda calculus, Coq, etc.) are branches of mathematics much like group theory,  model theory, number theory, geometries, etc.). 


My reason for not so much trusting theorem-proving isn't because I don't understand much of it (although that is a fact), but because of its formalism, which you obviously love. You consider most Axiom code (and by implication, mathematics on which it is based) as "hand-waving", which in my opinion, does not necessarily mean non-rigorous. Mathematicians frequently use "hand-waving" for results or methods or processes that are well-known (to experts, perhaps) so as not to make the argument too long and distract from the main one. So they use "it is easy to see", or "by induction", or "play the same game", etc.  


Believe it or not, theorem-proving use the same language and "hand-waving". Even Coq does the same if you look at its "proofs". See Proof for Lemmas 22 and 23, for example: "Both proofs go over easily by induction over the structure of the derivation." http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf


There is ​one exception: Whitehead and Russell's Principia Mathematica. Check this out (Wikipedia):


"Famously, several hundred pages of PM precede the proof of the validity of the proposition 1+1=2."


Now that is another form of "proving to the bare metal". Should we say, if we don't trust 1+1=2, then all is lost? No, ..., but ... (see Wiki):


"PM was an attempt to describe a set of axioms and inference rules in symbolic logic from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy,[1] being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, either the system must be inconsistent, or there must in fact be some truths of mathematics which could not be deduced from them."​

"The Principia covered only set theorycardinal numbersordinal numbers, and real numbers. Deeper theorems from real analysis were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be.

A fourth volume on the foundations of geometry had been planned, but the authors admitted to intellectual exhaustion upon completion of the third."


Perhaps someday, a more powerful computer system than Coq can reproduce PM (and prove its correctness, much like Coq proves the Four Color Theorem) and continue further. 

Nonetheless, even computers have their limits. 


That is why I suggest "good enough" is good enough. It is also why I admire your tenacity to follow your goal. Despite Gödel's incompleteness theorem, we need to prove correctness (of Axiom) as deep and wide as we can, and there are many ways to do that.


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: Tim Daly <[hidden email]>
Sent: Friday, April 6, 2018 6:34 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion.

I've spent a lot of time and study in the subject of understanding
better and less error-prone ways of programming. That has led me
to applying mathematics (ala Floyd/Hoare/Dijkstra). Given that
Axiom is about computational mathematics there is a natural goal of
trying to make Axiom better and less error-prone.

Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers.

My point of view is that writing Spad code that way is "pre-proof,
19th century 'hand-waving' mathematics". We can do better.

You obviously believe this is a waste of time. You are probably right.
But I've only got a few years left to waste and this seems to me to be
an important thing on which to waste them.

Tim


On Fri, Apr 6, 2018 at 1:23 AM, William Sit <[hidden email]> wrote:

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  



_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Tim Daly
>My reason for not so much trusting theorem-proving isn't because I don't
>understand much of it (although that is a fact), but because of its formalism
>which you obviously love.

Actually, I find the formalism to be painful and very non-intuitive.
Experience has shown me that it takes about 18 months to climb that
curve.

But consider that there are two VERY large areas of computational
mathematics that have grown up side-by-side for the last half-century.
CAS and Proof exist as essentially separate bodies of computational
mathematics.

My research effort is fundamentally about joining these two areas.

Proof systems can't use CAS results because they have no basis for trust.
They take stabs at algorithmic proofs but have no good structure to
combine them (which Axiom provides).

CAS systems don't do proofs, and in fact are nearly impossible to use
as a basis (MMA uses rewrite, Maple and others use ad hoc tree-like
structures, etc.)  Axiom provides a good basis for proofs.

Axiom is ideally structured to be a bridge.

Since I'm coming from the CAS world my view of bridge-building
involves applying Proof technology to Axiom. If I were coming from
the Proof world I'd be trying to structure a proof system along the
lines of Axiom so I could organize the proven algorithms. These are
two ends of the same bridge.




>You consder Axiom code (and by implication, mathematics on which it is
>based) as "hand-waving", which in my opinion, does not necessarily mean
>non-rigorous.

I don't consider the mathematics to be "hand-waving". But I do consider
the code to be hand-waving. After 47 years of programming I'm well aware
that "it works for my test cases" is a very poor measure of correctness.
There is a half-century of research that exists, is automated, and attacks
that question in a mathematically sound way.

Axiom code is rather opaque. It is, in general, excellent code. Barry and
James created an excellent structure for its time. But time has also shown
me the cracks. One example is the coercion code, a lot of which is ad hoc,
implemented as special cases in the interpreter. There are reasonable
theories about that which ought to be implemented.

I'm not trying to do anything new or innovative. I'm just trying to combine
what everyone does (on the proof side) with what everyone does (on the
CAS side). The end result should be of benefit to all of computational
mathematics.

Tim






On Fri, Apr 6, 2018 at 1:48 PM, William Sit <[hidden email]> wrote:

Dear Tim:


I never said, nor implied you are wasting your time. 


If there is any difference (and similarity) between our views, it is about trust. You do not trust Axiom code but you trust theorem-proving while I prefer to trust Axiom code and not so much on theorem-proving. Both research areas are mathematically based. Clearly, no one can in a life time understand all the mathematics behind these theories, and honestly, the theories in theorem-proving (including rewriting systems, type-theory, lambda calculus, Coq, etc.) are branches of mathematics much like group theory,  model theory, number theory, geometries, etc.). 


My reason for not so much trusting theorem-proving isn't because I don't understand much of it (although that is a fact), but because of its formalism, which you obviously love. You consider most Axiom code (and by implication, mathematics on which it is based) as "hand-waving", which in my opinion, does not necessarily mean non-rigorous. Mathematicians frequently use "hand-waving" for results or methods or processes that are well-known (to experts, perhaps) so as not to make the argument too long and distract from the main one. So they use "it is easy to see", or "by induction", or "play the same game", etc.  


Believe it or not, theorem-proving use the same language and "hand-waving". Even Coq does the same if you look at its "proofs". See Proof for Lemmas 22 and 23, for example: "Both proofs go over easily by induction over the structure of the derivation." http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf


There is ​one exception: Whitehead and Russell's Principia Mathematica. Check this out (Wikipedia):


"Famously, several hundred pages of PM precede the proof of the validity of the proposition 1+1=2."


Now that is another form of "proving to the bare metal". Should we say, if we don't trust 1+1=2, then all is lost? No, ..., but ... (see Wiki):


"PM was an attempt to describe a set of axioms and inference rules in symbolic logic from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy,[1] being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, either the system must be inconsistent, or there must in fact be some truths of mathematics which could not be deduced from them."​

"The Principia covered only set theorycardinal numbersordinal numbers, and real numbers. Deeper theorems from real analysis were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be.

A fourth volume on the foundations of geometry had been planned, but the authors admitted to intellectual exhaustion upon completion of the third."


Perhaps someday, a more powerful computer system than Coq can reproduce PM (and prove its correctness, much like Coq proves the Four Color Theorem) and continue further. 

Nonetheless, even computers have their limits. 


That is why I suggest "good enough" is good enough. It is also why I admire your tenacity to follow your goal. Despite Gödel's incompleteness theorem, we need to prove correctness (of Axiom) as deep and wide as we can, and there are many ways to do that.


William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Friday, April 6, 2018 6:34 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion.

I've spent a lot of time and study in the subject of understanding
better and less error-prone ways of programming. That has led me
to applying mathematics (ala Floyd/Hoare/Dijkstra). Given that
Axiom is about computational mathematics there is a natural goal of
trying to make Axiom better and less error-prone.

Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers.

My point of view is that writing Spad code that way is "pre-proof,
19th century 'hand-waving' mathematics". We can do better.

You obviously believe this is a waste of time. You are probably right.
But I've only got a few years left to waste and this seems to me to be
an important thing on which to waste them.

Tim


On Fri, Apr 6, 2018 at 1:23 AM, William Sit <[hidden email]> wrote:

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  




_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Tim Daly
Apropos of the coercion issue, Henri Tuhola just pointed me at a recent
PhD thesis by Stephen Dolan on Algebraic Subtyping:
https://www.cl.cam.ac.uk/~sd601/thesis.pdf

Tim


On Fri, Apr 6, 2018 at 4:04 PM, Tim Daly <[hidden email]> wrote:
>My reason for not so much trusting theorem-proving isn't because I don't
>understand much of it (although that is a fact), but because of its formalism
>which you obviously love.

Actually, I find the formalism to be painful and very non-intuitive.
Experience has shown me that it takes about 18 months to climb that
curve.

But consider that there are two VERY large areas of computational
mathematics that have grown up side-by-side for the last half-century.
CAS and Proof exist as essentially separate bodies of computational
mathematics.

My research effort is fundamentally about joining these two areas.

Proof systems can't use CAS results because they have no basis for trust.
They take stabs at algorithmic proofs but have no good structure to
combine them (which Axiom provides).

CAS systems don't do proofs, and in fact are nearly impossible to use
as a basis (MMA uses rewrite, Maple and others use ad hoc tree-like
structures, etc.)  Axiom provides a good basis for proofs.

Axiom is ideally structured to be a bridge.

Since I'm coming from the CAS world my view of bridge-building
involves applying Proof technology to Axiom. If I were coming from
the Proof world I'd be trying to structure a proof system along the
lines of Axiom so I could organize the proven algorithms. These are
two ends of the same bridge.




>You consder Axiom code (and by implication, mathematics on which it is
>based) as "hand-waving", which in my opinion, does not necessarily mean
>non-rigorous.

I don't consider the mathematics to be "hand-waving". But I do consider
the code to be hand-waving. After 47 years of programming I'm well aware
that "it works for my test cases" is a very poor measure of correctness.
There is a half-century of research that exists, is automated, and attacks
that question in a mathematically sound way.

Axiom code is rather opaque. It is, in general, excellent code. Barry and
James created an excellent structure for its time. But time has also shown
me the cracks. One example is the coercion code, a lot of which is ad hoc,
implemented as special cases in the interpreter. There are reasonable
theories about that which ought to be implemented.

I'm not trying to do anything new or innovative. I'm just trying to combine
what everyone does (on the proof side) with what everyone does (on the
CAS side). The end result should be of benefit to all of computational
mathematics.

Tim






On Fri, Apr 6, 2018 at 1:48 PM, William Sit <[hidden email]> wrote:

Dear Tim:


I never said, nor implied you are wasting your time. 


If there is any difference (and similarity) between our views, it is about trust. You do not trust Axiom code but you trust theorem-proving while I prefer to trust Axiom code and not so much on theorem-proving. Both research areas are mathematically based. Clearly, no one can in a life time understand all the mathematics behind these theories, and honestly, the theories in theorem-proving (including rewriting systems, type-theory, lambda calculus, Coq, etc.) are branches of mathematics much like group theory,  model theory, number theory, geometries, etc.). 


My reason for not so much trusting theorem-proving isn't because I don't understand much of it (although that is a fact), but because of its formalism, which you obviously love. You consider most Axiom code (and by implication, mathematics on which it is based) as "hand-waving", which in my opinion, does not necessarily mean non-rigorous. Mathematicians frequently use "hand-waving" for results or methods or processes that are well-known (to experts, perhaps) so as not to make the argument too long and distract from the main one. So they use "it is easy to see", or "by induction", or "play the same game", etc.  


Believe it or not, theorem-proving use the same language and "hand-waving". Even Coq does the same if you look at its "proofs". See Proof for Lemmas 22 and 23, for example: "Both proofs go over easily by induction over the structure of the derivation." http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf


There is ​one exception: Whitehead and Russell's Principia Mathematica. Check this out (Wikipedia):


"Famously, several hundred pages of PM precede the proof of the validity of the proposition 1+1=2."


Now that is another form of "proving to the bare metal". Should we say, if we don't trust 1+1=2, then all is lost? No, ..., but ... (see Wiki):


"PM was an attempt to describe a set of axioms and inference rules in symbolic logic from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy,[1] being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, either the system must be inconsistent, or there must in fact be some truths of mathematics which could not be deduced from them."​

"The Principia covered only set theorycardinal numbersordinal numbers, and real numbers. Deeper theorems from real analysis were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be.

A fourth volume on the foundations of geometry had been planned, but the authors admitted to intellectual exhaustion upon completion of the third."


Perhaps someday, a more powerful computer system than Coq can reproduce PM (and prove its correctness, much like Coq proves the Four Color Theorem) and continue further. 

Nonetheless, even computers have their limits. 


That is why I suggest "good enough" is good enough. It is also why I admire your tenacity to follow your goal. Despite Gödel's incompleteness theorem, we need to prove correctness (of Axiom) as deep and wide as we can, and there are many ways to do that.


William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Friday, April 6, 2018 6:34 AM

To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion.

I've spent a lot of time and study in the subject of understanding
better and less error-prone ways of programming. That has led me
to applying mathematics (ala Floyd/Hoare/Dijkstra). Given that
Axiom is about computational mathematics there is a natural goal of
trying to make Axiom better and less error-prone.

Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers.

My point of view is that writing Spad code that way is "pre-proof,
19th century 'hand-waving' mathematics". We can do better.

You obviously believe this is a waste of time. You are probably right.
But I've only got a few years left to waste and this seems to me to be
an important thing on which to waste them.

Tim


On Fri, Apr 6, 2018 at 1:23 AM, William Sit <[hidden email]> wrote:

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  





_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Tim Daly
I'd also include this, from Noam Zeilberger's PhD thesis:

    "The proofs-as-programs analogy really has demonstrated remarkable utility
    in driving progress in programming languages. Over the past few decades,
    many different ideas from logic have permeated into the field, reinterpreted
    from a computational perspective and collectively organized as type theory.
    In the 1980s, type theory dramatically improved the theoretical understanding
    of difficult language concepts such as absract data types and polymorphism,
    and led directly to the development of groundbreaking new languages such as
    ML and Haskell. In the other direction, type theory has also been applied back
    towards the mechanization of mathematics, and the Curry-Howard correspondence
    forms the basis for successful proof assistants such as Coq and Agda. Not least,
    the analogy between proving and programming has the social effect of linking
    two different communities of researchers: although people who write/study proofs
    and people who write/study programs often have very different motivations, the
    Curry-Howard correspondence says that in some ways they are doing very
    similar things."

The smart (of which I am not enough of) and elegant (of which I am not capable)
way to prove Axiom correct would be to fully exploit Curry-Howard in a way that
would make the programs BE the proofs. That's the correct way to approach this
problem. At my current state of understanding, this solution amounts to the old
blackboard joke of "insert a miracle here".

Tim


On Fri, Apr 6, 2018 at 4:50 PM, Tim Daly <[hidden email]> wrote:
Apropos of the coercion issue, Henri Tuhola just pointed me at a recent
PhD thesis by Stephen Dolan on Algebraic Subtyping:
https://www.cl.cam.ac.uk/~sd601/thesis.pdf

Tim


On Fri, Apr 6, 2018 at 4:04 PM, Tim Daly <[hidden email]> wrote:
>My reason for not so much trusting theorem-proving isn't because I don't
>understand much of it (although that is a fact), but because of its formalism
>which you obviously love.

Actually, I find the formalism to be painful and very non-intuitive.
Experience has shown me that it takes about 18 months to climb that
curve.

But consider that there are two VERY large areas of computational
mathematics that have grown up side-by-side for the last half-century.
CAS and Proof exist as essentially separate bodies of computational
mathematics.

My research effort is fundamentally about joining these two areas.

Proof systems can't use CAS results because they have no basis for trust.
They take stabs at algorithmic proofs but have no good structure to
combine them (which Axiom provides).

CAS systems don't do proofs, and in fact are nearly impossible to use
as a basis (MMA uses rewrite, Maple and others use ad hoc tree-like
structures, etc.)  Axiom provides a good basis for proofs.

Axiom is ideally structured to be a bridge.

Since I'm coming from the CAS world my view of bridge-building
involves applying Proof technology to Axiom. If I were coming from
the Proof world I'd be trying to structure a proof system along the
lines of Axiom so I could organize the proven algorithms. These are
two ends of the same bridge.




>You consder Axiom code (and by implication, mathematics on which it is
>based) as "hand-waving", which in my opinion, does not necessarily mean
>non-rigorous.

I don't consider the mathematics to be "hand-waving". But I do consider
the code to be hand-waving. After 47 years of programming I'm well aware
that "it works for my test cases" is a very poor measure of correctness.
There is a half-century of research that exists, is automated, and attacks
that question in a mathematically sound way.

Axiom code is rather opaque. It is, in general, excellent code. Barry and
James created an excellent structure for its time. But time has also shown
me the cracks. One example is the coercion code, a lot of which is ad hoc,
implemented as special cases in the interpreter. There are reasonable
theories about that which ought to be implemented.

I'm not trying to do anything new or innovative. I'm just trying to combine
what everyone does (on the proof side) with what everyone does (on the
CAS side). The end result should be of benefit to all of computational
mathematics.

Tim






On Fri, Apr 6, 2018 at 1:48 PM, William Sit <[hidden email]> wrote:

Dear Tim:


I never said, nor implied you are wasting your time. 


If there is any difference (and similarity) between our views, it is about trust. You do not trust Axiom code but you trust theorem-proving while I prefer to trust Axiom code and not so much on theorem-proving. Both research areas are mathematically based. Clearly, no one can in a life time understand all the mathematics behind these theories, and honestly, the theories in theorem-proving (including rewriting systems, type-theory, lambda calculus, Coq, etc.) are branches of mathematics much like group theory,  model theory, number theory, geometries, etc.). 


My reason for not so much trusting theorem-proving isn't because I don't understand much of it (although that is a fact), but because of its formalism, which you obviously love. You consider most Axiom code (and by implication, mathematics on which it is based) as "hand-waving", which in my opinion, does not necessarily mean non-rigorous. Mathematicians frequently use "hand-waving" for results or methods or processes that are well-known (to experts, perhaps) so as not to make the argument too long and distract from the main one. So they use "it is easy to see", or "by induction", or "play the same game", etc.  


Believe it or not, theorem-proving use the same language and "hand-waving". Even Coq does the same if you look at its "proofs". See Proof for Lemmas 22 and 23, for example: "Both proofs go over easily by induction over the structure of the derivation." http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf


There is ​one exception: Whitehead and Russell's Principia Mathematica. Check this out (Wikipedia):


"Famously, several hundred pages of PM precede the proof of the validity of the proposition 1+1=2."


Now that is another form of "proving to the bare metal". Should we say, if we don't trust 1+1=2, then all is lost? No, ..., but ... (see Wiki):


"PM was an attempt to describe a set of axioms and inference rules in symbolic logic from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy,[1] being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, either the system must be inconsistent, or there must in fact be some truths of mathematics which could not be deduced from them."​

"The Principia covered only set theorycardinal numbersordinal numbers, and real numbers. Deeper theorems from real analysis were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be.

A fourth volume on the foundations of geometry had been planned, but the authors admitted to intellectual exhaustion upon completion of the third."


Perhaps someday, a more powerful computer system than Coq can reproduce PM (and prove its correctness, much like Coq proves the Four Color Theorem) and continue further. 

Nonetheless, even computers have their limits. 


That is why I suggest "good enough" is good enough. It is also why I admire your tenacity to follow your goal. Despite Gödel's incompleteness theorem, we need to prove correctness (of Axiom) as deep and wide as we can, and there are many ways to do that.


William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Friday, April 6, 2018 6:34 AM

To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion.

I've spent a lot of time and study in the subject of understanding
better and less error-prone ways of programming. That has led me
to applying mathematics (ala Floyd/Hoare/Dijkstra). Given that
Axiom is about computational mathematics there is a natural goal of
trying to make Axiom better and less error-prone.

Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers.

My point of view is that writing Spad code that way is "pre-proof,
19th century 'hand-waving' mathematics". We can do better.

You obviously believe this is a waste of time. You are probably right.
But I've only got a few years left to waste and this seems to me to be
an important thing on which to waste them.

Tim


On Fri, Apr 6, 2018 at 1:23 AM, William Sit <[hidden email]> wrote:

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  






_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Tim Daly
I'm trying to figure out the most elegant way to put Spad on top of a
well-constructed set of theories. This would lead to some compiler
and interpreter changes to reduce the connection to practice.

There is a theory called the polymorphic lambda calculus (aka System F).
Whereas the lambda calculus allows us to make functions, the polymorphic
lambda calculus allows us to use types as parameters. We do this all the
time in Axiom, we just don't ground it in theory.

One possible path might be to re-host the Axiom compiler on an ML
backend (the intermediate backend). However, it is not yet clear to me
that ML can handle Axiom's coercions and conversions. So far I have
not found anything that can. I might need to write a second survey paper.
At the moment I'm reading the ML compiler source code.

There is work by Dolan (Dola17) on Algebraic Subtyping which might
handle part of it but I'm still working my way through his thesis.

Tim


On Fri, Apr 6, 2018 at 5:44 PM, Tim Daly <[hidden email]> wrote:
I'd also include this, from Noam Zeilberger's PhD thesis:

    "The proofs-as-programs analogy really has demonstrated remarkable utility
    in driving progress in programming languages. Over the past few decades,
    many different ideas from logic have permeated into the field, reinterpreted
    from a computational perspective and collectively organized as type theory.
    In the 1980s, type theory dramatically improved the theoretical understanding
    of difficult language concepts such as absract data types and polymorphism,
    and led directly to the development of groundbreaking new languages such as
    ML and Haskell. In the other direction, type theory has also been applied back
    towards the mechanization of mathematics, and the Curry-Howard correspondence
    forms the basis for successful proof assistants such as Coq and Agda. Not least,
    the analogy between proving and programming has the social effect of linking
    two different communities of researchers: although people who write/study proofs
    and people who write/study programs often have very different motivations, the
    Curry-Howard correspondence says that in some ways they are doing very
    similar things."

The smart (of which I am not enough of) and elegant (of which I am not capable)
way to prove Axiom correct would be to fully exploit Curry-Howard in a way that
would make the programs BE the proofs. That's the correct way to approach this
problem. At my current state of understanding, this solution amounts to the old
blackboard joke of "insert a miracle here".

Tim


On Fri, Apr 6, 2018 at 4:50 PM, Tim Daly <[hidden email]> wrote:
Apropos of the coercion issue, Henri Tuhola just pointed me at a recent
PhD thesis by Stephen Dolan on Algebraic Subtyping:
https://www.cl.cam.ac.uk/~sd601/thesis.pdf

Tim


On Fri, Apr 6, 2018 at 4:04 PM, Tim Daly <[hidden email]> wrote:
>My reason for not so much trusting theorem-proving isn't because I don't
>understand much of it (although that is a fact), but because of its formalism
>which you obviously love.

Actually, I find the formalism to be painful and very non-intuitive.
Experience has shown me that it takes about 18 months to climb that
curve.

But consider that there are two VERY large areas of computational
mathematics that have grown up side-by-side for the last half-century.
CAS and Proof exist as essentially separate bodies of computational
mathematics.

My research effort is fundamentally about joining these two areas.

Proof systems can't use CAS results because they have no basis for trust.
They take stabs at algorithmic proofs but have no good structure to
combine them (which Axiom provides).

CAS systems don't do proofs, and in fact are nearly impossible to use
as a basis (MMA uses rewrite, Maple and others use ad hoc tree-like
structures, etc.)  Axiom provides a good basis for proofs.

Axiom is ideally structured to be a bridge.

Since I'm coming from the CAS world my view of bridge-building
involves applying Proof technology to Axiom. If I were coming from
the Proof world I'd be trying to structure a proof system along the
lines of Axiom so I could organize the proven algorithms. These are
two ends of the same bridge.




>You consder Axiom code (and by implication, mathematics on which it is
>based) as "hand-waving", which in my opinion, does not necessarily mean
>non-rigorous.

I don't consider the mathematics to be "hand-waving". But I do consider
the code to be hand-waving. After 47 years of programming I'm well aware
that "it works for my test cases" is a very poor measure of correctness.
There is a half-century of research that exists, is automated, and attacks
that question in a mathematically sound way.

Axiom code is rather opaque. It is, in general, excellent code. Barry and
James created an excellent structure for its time. But time has also shown
me the cracks. One example is the coercion code, a lot of which is ad hoc,
implemented as special cases in the interpreter. There are reasonable
theories about that which ought to be implemented.

I'm not trying to do anything new or innovative. I'm just trying to combine
what everyone does (on the proof side) with what everyone does (on the
CAS side). The end result should be of benefit to all of computational
mathematics.

Tim






On Fri, Apr 6, 2018 at 1:48 PM, William Sit <[hidden email]> wrote:

Dear Tim:


I never said, nor implied you are wasting your time. 


If there is any difference (and similarity) between our views, it is about trust. You do not trust Axiom code but you trust theorem-proving while I prefer to trust Axiom code and not so much on theorem-proving. Both research areas are mathematically based. Clearly, no one can in a life time understand all the mathematics behind these theories, and honestly, the theories in theorem-proving (including rewriting systems, type-theory, lambda calculus, Coq, etc.) are branches of mathematics much like group theory,  model theory, number theory, geometries, etc.). 


My reason for not so much trusting theorem-proving isn't because I don't understand much of it (although that is a fact), but because of its formalism, which you obviously love. You consider most Axiom code (and by implication, mathematics on which it is based) as "hand-waving", which in my opinion, does not necessarily mean non-rigorous. Mathematicians frequently use "hand-waving" for results or methods or processes that are well-known (to experts, perhaps) so as not to make the argument too long and distract from the main one. So they use "it is easy to see", or "by induction", or "play the same game", etc.  


Believe it or not, theorem-proving use the same language and "hand-waving". Even Coq does the same if you look at its "proofs". See Proof for Lemmas 22 and 23, for example: "Both proofs go over easily by induction over the structure of the derivation." http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf


There is ​one exception: Whitehead and Russell's Principia Mathematica. Check this out (Wikipedia):


"Famously, several hundred pages of PM precede the proof of the validity of the proposition 1+1=2."


Now that is another form of "proving to the bare metal". Should we say, if we don't trust 1+1=2, then all is lost? No, ..., but ... (see Wiki):


"PM was an attempt to describe a set of axioms and inference rules in symbolic logic from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy,[1] being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, either the system must be inconsistent, or there must in fact be some truths of mathematics which could not be deduced from them."​

"The Principia covered only set theorycardinal numbersordinal numbers, and real numbers. Deeper theorems from real analysis were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be.

A fourth volume on the foundations of geometry had been planned, but the authors admitted to intellectual exhaustion upon completion of the third."


Perhaps someday, a more powerful computer system than Coq can reproduce PM (and prove its correctness, much like Coq proves the Four Color Theorem) and continue further. 

Nonetheless, even computers have their limits. 


That is why I suggest "good enough" is good enough. It is also why I admire your tenacity to follow your goal. Despite Gödel's incompleteness theorem, we need to prove correctness (of Axiom) as deep and wide as we can, and there are many ways to do that.


William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Friday, April 6, 2018 6:34 AM

To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion.

I've spent a lot of time and study in the subject of understanding
better and less error-prone ways of programming. That has led me
to applying mathematics (ala Floyd/Hoare/Dijkstra). Given that
Axiom is about computational mathematics there is a natural goal of
trying to make Axiom better and less error-prone.

Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers.

My point of view is that writing Spad code that way is "pre-proof,
19th century 'hand-waving' mathematics". We can do better.

You obviously believe this is a waste of time. You are probably right.
But I've only got a few years left to waste and this seems to me to be
an important thing on which to waste them.

Tim


On Fri, Apr 6, 2018 at 1:23 AM, William Sit <[hidden email]> wrote:

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  







_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Proving Axiom Correct

Henri Tuhola
The type-indeterminate idea I have attempts to answer what to do when you can single-dispatch, but you have a binary operation and two different types.

The idea is that indeterminate variables exist before type inference, and they are linked to their respective representations. The dispatch to be done is then determined by approximating the return type.

The return type is approximated by retrieving the indeterminate variables and producing a single type that contains them all. It's easiest to explain my an example:

If you have addition with Polynomial[x](Complex[i](Float())) on the left side, and Matrix[t](2, 2, Complex[i](Float())) on the right side. Start approximating the return type.

The indeterminates on left side {x, i}, and on the right side {t,i}. The union of these is {t,x,i}. These are mapped to types: {t: Matrix, x:Polynomial, i:Complex}. Therefore the return type is: Matrix[t](2, 2, Polynomial[x](Complex[i](Float()))).

Next the sides are converted into the return type and the single dispatch is done for the return type to retrieve the implementation for addition. Nicolas Doye's paper presents how the conversion can be done.

I got a problem here though.. It's that I'm not sure about whether this approach works.


-- Henri Tuhola



On 8 April 2018 at 23:49, Tim Daly <[hidden email]> wrote:
I'm trying to figure out the most elegant way to put Spad on top of a
well-constructed set of theories. This would lead to some compiler
and interpreter changes to reduce the connection to practice.

There is a theory called the polymorphic lambda calculus (aka System F).
Whereas the lambda calculus allows us to make functions, the polymorphic
lambda calculus allows us to use types as parameters. We do this all the
time in Axiom, we just don't ground it in theory.

One possible path might be to re-host the Axiom compiler on an ML
backend (the intermediate backend). However, it is not yet clear to me
that ML can handle Axiom's coercions and conversions. So far I have
not found anything that can. I might need to write a second survey paper.
At the moment I'm reading the ML compiler source code.

There is work by Dolan (Dola17) on Algebraic Subtyping which might
handle part of it but I'm still working my way through his thesis.

Tim


On Fri, Apr 6, 2018 at 5:44 PM, Tim Daly <[hidden email]> wrote:
I'd also include this, from Noam Zeilberger's PhD thesis:

    "The proofs-as-programs analogy really has demonstrated remarkable utility
    in driving progress in programming languages. Over the past few decades,
    many different ideas from logic have permeated into the field, reinterpreted
    from a computational perspective and collectively organized as type theory.
    In the 1980s, type theory dramatically improved the theoretical understanding
    of difficult language concepts such as absract data types and polymorphism,
    and led directly to the development of groundbreaking new languages such as
    ML and Haskell. In the other direction, type theory has also been applied back
    towards the mechanization of mathematics, and the Curry-Howard correspondence
    forms the basis for successful proof assistants such as Coq and Agda. Not least,
    the analogy between proving and programming has the social effect of linking
    two different communities of researchers: although people who write/study proofs
    and people who write/study programs often have very different motivations, the
    Curry-Howard correspondence says that in some ways they are doing very
    similar things."

The smart (of which I am not enough of) and elegant (of which I am not capable)
way to prove Axiom correct would be to fully exploit Curry-Howard in a way that
would make the programs BE the proofs. That's the correct way to approach this
problem. At my current state of understanding, this solution amounts to the old
blackboard joke of "insert a miracle here".

Tim


On Fri, Apr 6, 2018 at 4:50 PM, Tim Daly <[hidden email]> wrote:
Apropos of the coercion issue, Henri Tuhola just pointed me at a recent
PhD thesis by Stephen Dolan on Algebraic Subtyping:
https://www.cl.cam.ac.uk/~sd601/thesis.pdf

Tim


On Fri, Apr 6, 2018 at 4:04 PM, Tim Daly <[hidden email]> wrote:
>My reason for not so much trusting theorem-proving isn't because I don't
>understand much of it (although that is a fact), but because of its formalism
>which you obviously love.

Actually, I find the formalism to be painful and very non-intuitive.
Experience has shown me that it takes about 18 months to climb that
curve.

But consider that there are two VERY large areas of computational
mathematics that have grown up side-by-side for the last half-century.
CAS and Proof exist as essentially separate bodies of computational
mathematics.

My research effort is fundamentally about joining these two areas.

Proof systems can't use CAS results because they have no basis for trust.
They take stabs at algorithmic proofs but have no good structure to
combine them (which Axiom provides).

CAS systems don't do proofs, and in fact are nearly impossible to use
as a basis (MMA uses rewrite, Maple and others use ad hoc tree-like
structures, etc.)  Axiom provides a good basis for proofs.

Axiom is ideally structured to be a bridge.

Since I'm coming from the CAS world my view of bridge-building
involves applying Proof technology to Axiom. If I were coming from
the Proof world I'd be trying to structure a proof system along the
lines of Axiom so I could organize the proven algorithms. These are
two ends of the same bridge.




>You consder Axiom code (and by implication, mathematics on which it is
>based) as "hand-waving", which in my opinion, does not necessarily mean
>non-rigorous.

I don't consider the mathematics to be "hand-waving". But I do consider
the code to be hand-waving. After 47 years of programming I'm well aware
that "it works for my test cases" is a very poor measure of correctness.
There is a half-century of research that exists, is automated, and attacks
that question in a mathematically sound way.

Axiom code is rather opaque. It is, in general, excellent code. Barry and
James created an excellent structure for its time. But time has also shown
me the cracks. One example is the coercion code, a lot of which is ad hoc,
implemented as special cases in the interpreter. There are reasonable
theories about that which ought to be implemented.

I'm not trying to do anything new or innovative. I'm just trying to combine
what everyone does (on the proof side) with what everyone does (on the
CAS side). The end result should be of benefit to all of computational
mathematics.

Tim






On Fri, Apr 6, 2018 at 1:48 PM, William Sit <[hidden email]> wrote:

Dear Tim:


I never said, nor implied you are wasting your time. 


If there is any difference (and similarity) between our views, it is about trust. You do not trust Axiom code but you trust theorem-proving while I prefer to trust Axiom code and not so much on theorem-proving. Both research areas are mathematically based. Clearly, no one can in a life time understand all the mathematics behind these theories, and honestly, the theories in theorem-proving (including rewriting systems, type-theory, lambda calculus, Coq, etc.) are branches of mathematics much like group theory,  model theory, number theory, geometries, etc.). 


My reason for not so much trusting theorem-proving isn't because I don't understand much of it (although that is a fact), but because of its formalism, which you obviously love. You consider most Axiom code (and by implication, mathematics on which it is based) as "hand-waving", which in my opinion, does not necessarily mean non-rigorous. Mathematicians frequently use "hand-waving" for results or methods or processes that are well-known (to experts, perhaps) so as not to make the argument too long and distract from the main one. So they use "it is easy to see", or "by induction", or "play the same game", etc.  


Believe it or not, theorem-proving use the same language and "hand-waving". Even Coq does the same if you look at its "proofs". See Proof for Lemmas 22 and 23, for example: "Both proofs go over easily by induction over the structure of the derivation." http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf


There is ​one exception: Whitehead and Russell's Principia Mathematica. Check this out (Wikipedia):


"Famously, several hundred pages of PM precede the proof of the validity of the proposition 1+1=2."


Now that is another form of "proving to the bare metal". Should we say, if we don't trust 1+1=2, then all is lost? No, ..., but ... (see Wiki):


"PM was an attempt to describe a set of axioms and inference rules in symbolic logic from which all mathematical truths could in principle be proven. As such, this ambitious project is of great importance in the history of mathematics and philosophy,[1] being one of the foremost products of the belief that such an undertaking may be achievable. However, in 1931, Gödel's incompleteness theorem proved definitively that PM, and in fact any other attempt, could never achieve this lofty goal; that is, for any set of axioms and inference rules proposed to encapsulate mathematics, either the system must be inconsistent, or there must in fact be some truths of mathematics which could not be deduced from them."​

"The Principia covered only set theorycardinal numbersordinal numbers, and real numbers. Deeper theorems from real analysis were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could in principle be developed in the adopted formalism. It was also clear how lengthy such a development would be.

A fourth volume on the foundations of geometry had been planned, but the authors admitted to intellectual exhaustion upon completion of the third."


Perhaps someday, a more powerful computer system than Coq can reproduce PM (and prove its correctness, much like Coq proves the Four Color Theorem) and continue further. 

Nonetheless, even computers have their limits. 


That is why I suggest "good enough" is good enough. It is also why I admire your tenacity to follow your goal. Despite Gödel's incompleteness theorem, we need to prove correctness (of Axiom) as deep and wide as we can, and there are many ways to do that.


William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Friday, April 6, 2018 6:34 AM

To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
One lesson I have learned over all my years is that you'd can't ever
change people's minds by argument or discussion.

I've spent a lot of time and study in the subject of understanding
better and less error-prone ways of programming. That has led me
to applying mathematics (ala Floyd/Hoare/Dijkstra). Given that
Axiom is about computational mathematics there is a natural goal of
trying to make Axiom better and less error-prone.

Proving Axiom correct is a very challenging and not very popular idea.
Writing Spad code is hard. Proving the code correct is beyond the
skill of most programmers. Sadly, even writing words to explain how
the code works seems beyond the skill of most programmers.

My point of view is that writing Spad code that way is "pre-proof,
19th century 'hand-waving' mathematics". We can do better.

You obviously believe this is a waste of time. You are probably right.
But I've only got a few years left to waste and this seems to me to be
an important thing on which to waste them.

Tim


On Fri, Apr 6, 2018 at 1:23 AM, William Sit <[hidden email]> wrote:

Dear Tim:


Thanks again for taking the time to explain your efforts and to further my understanding on the issue of proving "down to the metal". By following all the leads you gave, I had a quick course.


Unfortunately, despite the tremendous efforts in the computing industry to assure us of correctness ("proven" by formalism), at least from what you wrote (which I understand was not meant to be comprehensive), not only are those efforts piecewise, they also concentrate on quite limited aspects.


My comments are in regular font; italicized paragraphs are quoted passages, isolated italics and highlights are mine. Itemized headings are from your email.


1. BLAS/LAPACK: they use a lot of coding tricks to avoid overflow/underflow/significance loss/etc​.


Coding tricks are adverse to proofs by formal logics, or at least such code makes it practically impossible to assure correctness. Most of the time, these tricks are patches to deal with post-implementation revealed bugs (whose discoveries are more from real-life usage than from program proving).


2. Field Programmable Gate Array (FPGA)


These are great at the gate level and of course, theoretically, they are the basic blocks in building Turing machines (practically, finite state machines or FSMs). Mealy/Moore state machines are just two ways to look at FSMs; I read 

and there are nice examples illustrating the steps to construct FSMs (a bit of a nostalgic trip to revisit Karnaugh maps I learned in the 1970s) .  I assume these applications can all be automated and proven correct once the set of specifications for the finite state machine to perform a task is given but the final correctness still depend on a proven set of specifications! As far as I can discern, specifications are done manually since they are task dependent.
As an example, before proving that a compiler is correct implemented, one needs to specify the language and the compiling algorithm (which of course, can be and have been done, like YACC). Despite all the verification and our trust in the proof algorithms and implementations, there remains a small probability that something may still be amiss in the specifications, like an unanticipated but grammatically correct input is diagnosed as an error. We have all seen compiler error messages that do not pinpoint where the error originated.

I read that, and my understanding is that these proven microkernels are concerned with security (both from external and from internal threats) in multicore architectures (which are prevalent in all CPU designs nowadays) and multi- and coexisting OSes. Even under such a general yet limited aspect of "proven correctness" (by formalism no less), there is no guarantee (paragraph under: Formally Proven Security):

In order to achieve the highest level of security, ProvenVisor uses a microkernel architecture implemented using formally proven code to get as close as possible to zero-defects, to guarantee the expected security properties and to ease the path to any required certifications. This architecture and the formal proofs insure the sustainability of the maintenance process of systems based on ProvenVisor. ... 

This may be legalese, but from the highlighted phrases clearly show that the goal is not "proven and complete specifications" on security. Even the formally proven code does not guarantee zero-defects on expected violations.  It is only a "best effort" (which still is commendable). The scope is also limited:

Prove & Run’s formal software development toolchain. This means that it is mathematically proven that virtual machines (VMs) hosted by ProvenVisor will always retain their integrity (no other VM can tamper with their internal data) and confidentiality (no other VM can read their internal data). A misbehaving or malicious OS has no way to modify another OS or to spy on another OS.

A malicious program need not run in a hosted OS or VM if it gains access to the microkernel, say with an external hardware (and external software) that can modify it. After all, there has to be such equipment to test whether the microkernel is working or not and to apply patches if need be.

And a major "professional service" offered is:
Revamping existing architectures for security with ad-hoc solutions: Secure Boot, secure Over-the-Air firmware update, firewalling, intrusion detection/protection solutions, authentication, secure storage, etc…

Does "ad-hoc solutions" mean patches?

4. The issue of Trust: If you can't trust the hardware gates to compute a valid AND/OR/NOT then all is lost.

Actually, I not only trust, but also believe in the correctness, or proof thereof, of gate-level logic or a microkernel, but that is a far far cry from, say, my trust in the correctness of an implementation of the Risch algorithm or Kovacic's algorithm. The complexity of coding high level symbolic algebraic methods, when traced down to the metal, as you say, is beyond current proof technology (nor is there sufficient interest in the hardware industry to provide that level of research). Note that the industry is still satisfied with "ad-hoc solutions" (and that might mean patches, and we all know how error-prone those are---so much so that people learn and re-invent the wheel over and over again for a better wheel).

Can prove-technology catch up, ever?

I know I can't catch up. Still ignorant and biased.

William


William Sit
Professor Emeritus
Department of Mathematics
The City College of The City University of New York
New York, NY 10031

From: Tim Daly <[hidden email]>
Sent: Thursday, April 5, 2018 2:59 AM
To: William Sit
Cc: axiom-dev; Tim Daly
Subject: Re: [Axiom-developer] Proving Axiom Correct
 
William,

I understand the issue of proving "down to the metal".

Axiom's Volume 10.5 has my implementation of the BLAS / LAPACK
libraries in Common Lisp. Those libraries have a lot of coding tricks
to avoid overflow/underflow/significance loss/etc.

Two years ago I got Gustafson's "End of Error" book. His new floating
point format promises to eliminate these kinds of errors. Unfortunately
no current processor implements his instructions.

So I bought an Altera Cyclone Field Programmable Gate Array (FPGA)
in order to implement the hardware instructions. This is my setup at home:
http://daly.axiom-developer.org/FPGA1.jpg
http://daly.axiom-developer.org/FPGA2.jpg
http://daly.axiom-developer.org/FPGA3.jpg
http://daly.axiom-developre.org/FPGA4.jpg
This is not yet published work.

The game is to implement the instructions at the hardware gate level
using Mealy/Moore state machines. Since this is a clocked logic design
the state machines can be modelled as Turing machines.

This allows Gustafson's arithmetic to be a real hardware processor.

It turns out that shortly after I bought the FPGA from Altera (2 years ago)
Intel bought Altera. They have recently released a new chip that combines
the CPU and FPGA
https://www.intel.com/content/www/us/en/fpga/devices.html

Unfortunately the new chip is only available to data centers in server
machines and I can't buy one (nor can I afford it). But this would allow
Gustafson arithmetic at the hardware level.

My Altera Cyclone has 2 ARM processors built into the chip. ProvenVisor
has a verified hypervisor running on the ARM core
http://www.provenrun.com/products/provenvisor/nxp/

So I've looked at the issue all the way down to the gate-level hardware
which is boolean logic and Turing machine level proofs.

It all eventually comes down to trust but I'm not sure what else I can do
to ensure that the proofs are trustworthy. If you can't trust the hardware
gates to compute a valid AND/OR/NOT then all is lost.

Tim


On Wed, Apr 4, 2018 at 6:03 PM, William Sit <[hidden email]> wrote:
...

[Message clipped]  







_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer



_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer