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 <axiom...@gmail.com> 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 <w...@ccny.cuny.edu> 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.po >> lytechnique.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 >> <https://en.wikipedia.org/wiki/Axiom> and inference rules >> <https://en.wikipedia.org/wiki/Inference_rule> in symbolic logic >> <https://en.wikipedia.org/wiki/Mathematical_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] <https://en.wikipedia.org/wiki/Principia_Mathematica#cite_note-SEP-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 >> <https://en.wikipedia.org/wiki/G%C3%B6del%27s_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 theory >> <https://en.wikipedia.org/wiki/Set_theory>, cardinal numbers >> <https://en.wikipedia.org/wiki/Cardinal_numbers>, ordinal numbers >> <https://en.wikipedia.org/wiki/Ordinal_numbers>, and real numbers >> <https://en.wikipedia.org/wiki/Real_numbers>. Deeper theorems from real >> analysis <https://en.wikipedia.org/wiki/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 >> <https://en.wikipedia.org/wiki/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 >> <https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorem>'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 <axiom...@gmail.com> >> *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 <w...@ccny.cuny.edu> 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 >>> www-inst.eecs.berkeley.edu/~cs150/fa05/Lectures/07-SeqLogicIIIx2.pdf >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__www-2Dinst.eecs.berkeley.edu_-7Ecs150_fa05_Lectures_07-2DSeqLogicIIIx2.pdf&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=KxTLI8x_XLCw7f5LfxLdI49gcxkIWNLTXuBtYg0NHEg&s=szqaazDR95Wrn7_jCR-l2FRtSdu-JPzQaOKz3DrgM7s&e=> >>> >>> <https://urldefense.proofpoint.com/v2/url?u=https-3A__www.google.com_search-3Fclient-3Dsafari-26rls-3Den-26q-3DMealy_Moore-2Bstate-2Bmachines-26ie-3DUTF-2D8-26oe-3DUTF-2D8-23&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=KxTLI8x_XLCw7f5LfxLdI49gcxkIWNLTXuBtYg0NHEg&s=1lAmJKR4Fh7uaDIgVGCV-TOG2A9nKHvvLcg0okuMRQc&e=> >>> >>> 1. >>> >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__webcache.googleusercontent.com_search-3Fq-3Dcache-3AuM-5FBbEPaPGoJ-3Awww-2Dinst.eecs.berkeley.edu_-7Ecs150_fa05_Lectures_07-2DSeqLogicIIIx2.pdf-2B-26cd-3D6-26hl-3Den-26ct-3Dclnk-26gl-3Dus-26client-3Dsafari&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=KxTLI8x_XLCw7f5LfxLdI49gcxkIWNLTXuBtYg0NHEg&s=u_SL_Yp7SymLcIYBuRwEeVwmSIbRJKmM7YSI_pzoFKI&e=> >>> >>> 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. >>> >>> 3. ProvenVisor on ARMs. http://www.provenrun.com >>> /products/provenvisor/nxp/ >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__www.provenrun.com_products_provenvisor_nxp_&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=KxTLI8x_XLCw7f5LfxLdI49gcxkIWNLTXuBtYg0NHEg&s=s_pEqwh0zu3dxsLS4ULymJ-AlzLujST5uQgG6v63lGQ&e=> >>> >>> 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 <axiom...@gmail.com> >>> *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. >>> http://axiom-developer.org/axiom-website/bookvol10.5.pdf >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__axiom-2Ddeveloper.org_axiom-2Dwebsite_bookvol10.5.pdf&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=TfKyDJSqnnlVceWTEzW9xokZ1KC93faNl5VIDbb9UcI&s=mpk34qrWk3WJGr_ccjQTRsRc3coNGefE5fxMBHyOVR8&e=> >>> >>> 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 >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__daly.axiom-2Ddeveloper.org_FPGA1.jpg&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=TfKyDJSqnnlVceWTEzW9xokZ1KC93faNl5VIDbb9UcI&s=009W3KhNl-v5TU61jwX3DxojKkmBinurdVU-ywxJFR8&e=> >>> http://daly.axiom-developer.org/FPGA2.jpg >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__daly.axiom-2Ddeveloper.org_FPGA2.jpg&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=TfKyDJSqnnlVceWTEzW9xokZ1KC93faNl5VIDbb9UcI&s=cBM4oaXxsJKB_XWealTIwgYY5LNXwX1RgmZdwEnOmFQ&e=> >>> http://daly.axiom-developer.org/FPGA3.jpg >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__daly.axiom-2Ddeveloper.org_FPGA3.jpg&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=TfKyDJSqnnlVceWTEzW9xokZ1KC93faNl5VIDbb9UcI&s=JjPVQ8eaQpifo_U2CARxxWczJaCDM7kaTsQHkFsi2wI&e=> >>> http://daly.axiom-developre.org/FPGA4.jpg >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__daly.axiom-2Ddevelopre.org_FPGA4.jpg&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=TfKyDJSqnnlVceWTEzW9xokZ1KC93faNl5VIDbb9UcI&s=AVSMfPcPADQNdLQEz9y31ObEtrWVqgIdjs_W9All2K8&e=> >>> 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 >>> <https://urldefense.proofpoint.com/v2/url?u=https-3A__www.intel.com_content_www_us_en_fpga_devices.html&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=TfKyDJSqnnlVceWTEzW9xokZ1KC93faNl5VIDbb9UcI&s=GDFziH4XPpntP4Bx6JYWPEz7olCOacUZp7NpsnNtQsQ&e=> >>> >>> 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/ >>> <https://urldefense.proofpoint.com/v2/url?u=http-3A__www.provenrun.com_products_provenvisor_nxp_&d=DwMFaQ&c=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo&r=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU&m=TfKyDJSqnnlVceWTEzW9xokZ1KC93faNl5VIDbb9UcI&s=QGxWqtU50kOphUY1RkRhn4fkDttKVTN2ndMpbBVqB5M&e=> >>> >>> 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 <w...@ccny.cuny.edu> wrote: >>> >>>> ... >>>> >>>> [Message clipped] >>> >>> >>> >> >
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
