Re: [EXTERNAL] Re: Axiom musings...
The goal is to prove Axiom algorithms, such as the GCD over the natural numbers, correct using something like Lean. I've studied traditional approaches like Hoare triples but I think there might be a different approach. It depends on Harper's Trinity. Suppose I had a set of verification conditions V. Suppose I had a functor that carries V to a program P. Suppose I had a functor that carries V to a proof Q. By the category definition of functors this implies a natural transformation between P and Q ... and I'm done. Except for some annoying details, of course. 1) What is a functor from V to P? Well, I have all of group theory already available because of the way Axiom is constructed. So the "elements" of the functor requires things like "carrying identity". Exactly what this implies in the constructed program P needs to be worked out in detail. 2) What is the functor from V to Q? Well, if I construct a sequent calculus version of Lean's Type Theory then I have a "complete" set of low-level tactics. It isn't clear how those tactics can be applied to construct the functor (at least not yet). 3) The two functors require certain constraints on the verification conditions V. In dealing with the GCD over the natural numbers (known as NonNegativeInteger or NNI in Axiom) we need to make sure that V contains all of the conditions that the correct program requires (such as deriving the recursive call). 4) V also needs constraints in dealing with the GCD so that the proof can use the Lean sequent rules to derive a proof of the GCD. So I'd have to construct a sequent proof of the GCD from the sequent-derived tactics. 5) I don't know of a languge V that covers both the needs of the functors for P and Q so that will take some omphaloskepsis. I might have to write a "linter" program. This category theory approach, using Harper's Trinity, has the potential of proving programs correct without dealing with things like Hoare triples. This all works in theory but there is a lot of practical work, such as deriving a sequent form of Lean's Type Theory, deriving functors that fulfill all the definitions using things like Axiom's group theory structure, and inventing the verification language V rich enough for both needs. It's gonna be a long winter :-) Tim . On 12/18/20, Tim Daly wrote: > Quoting Dijkstra (1988, EWD1036): > > ... a program is no more than half a conjecture. The other > half of a conjecture is the functional specification the > program is supposed to satisfy. The programmer's task > is to present such complete conjectures as proven theorems. > > > Axiom's SANE research project is trying to build a system > where such "complete conjectures as proven theorems" > can be implemented, at least for mathematical algorithms. > > After 50 years of programming it is humbling to realize > that I've neglected the most important half of programming. > > The amount of effort and progress in proof theory, category > theory, and interactive theorem proving is amazing; most > of it only occuring in this century. I've spent the last 8 years > trying to "catch up" with what future programmers will take > as normal and expected. > > Imagine a Google whiteboard interview where you are > asked to provide an algorithm and an associated proof. > Will you get hired? > > Dijkstra saw this in 1988 and it's taken me decades to > hear and understand. > > Tim > > > On 12/18/20, Tim Daly wrote: >> I occasionally get grief because Axiom is implemented >> in Common Lisp. People don't seem to like that for some >> odd reason. Lisp, one of the easiest languages to learn, >> seems to be difficult to accept. >> >> I'm working with John Harrison's book "Practical Logic >> and Automated Reasoning" from 2009. It uses OCaml >> to implement the programs. >> >> I've downloaded the OCaml sources from the website. >> Apparently OCaml has changed significantly from 2009 >> since the code no longer compiles, spitting out "Alert >> deprecated" all over the place and simply failing in places. >> >> C++ code has a "standard", well, several "standards". >> When someone asks "Do you know C++" you really >> need to qualify that question. What you knew about >> "standard C++" seems to change every 2 years. >> >> I recently pulled out my KROPS code, used as the >> basis for IBM's Expert System FAME. It was written >> in Common Lisp (on a Symbolics machine). It still runs >> unmodified despite being written about 40 years ago >> on hardware and a software stack that no longer exists. >> >> Axiom, written in the last century, still compiles and >> runs. Say what you want about Lisp code, it still is the >> most portable and long-lasting language I've ever used. >> >> Tim >> >
Re: [EXTERNAL] Re: Axiom musings...
Quoting Dijkstra (1988, EWD1036): ... a program is no more than half a conjecture. The other half of a conjecture is the functional specification the program is supposed to satisfy. The programmer's task is to present such complete conjectures as proven theorems. Axiom's SANE research project is trying to build a system where such "complete conjectures as proven theorems" can be implemented, at least for mathematical algorithms. After 50 years of programming it is humbling to realize that I've neglected the most important half of programming. The amount of effort and progress in proof theory, category theory, and interactive theorem proving is amazing; most of it only occuring in this century. I've spent the last 8 years trying to "catch up" with what future programmers will take as normal and expected. Imagine a Google whiteboard interview where you are asked to provide an algorithm and an associated proof. Will you get hired? Dijkstra saw this in 1988 and it's taken me decades to hear and understand. Tim On 12/18/20, Tim Daly wrote: > I occasionally get grief because Axiom is implemented > in Common Lisp. People don't seem to like that for some > odd reason. Lisp, one of the easiest languages to learn, > seems to be difficult to accept. > > I'm working with John Harrison's book "Practical Logic > and Automated Reasoning" from 2009. It uses OCaml > to implement the programs. > > I've downloaded the OCaml sources from the website. > Apparently OCaml has changed significantly from 2009 > since the code no longer compiles, spitting out "Alert > deprecated" all over the place and simply failing in places. > > C++ code has a "standard", well, several "standards". > When someone asks "Do you know C++" you really > need to qualify that question. What you knew about > "standard C++" seems to change every 2 years. > > I recently pulled out my KROPS code, used as the > basis for IBM's Expert System FAME. It was written > in Common Lisp (on a Symbolics machine). It still runs > unmodified despite being written about 40 years ago > on hardware and a software stack that no longer exists. > > Axiom, written in the last century, still compiles and > runs. Say what you want about Lisp code, it still is the > most portable and long-lasting language I've ever used. > > Tim >
Re: [EXTERNAL] Re: Axiom musings...
I occasionally get grief because Axiom is implemented in Common Lisp. People don't seem to like that for some odd reason. Lisp, one of the easiest languages to learn, seems to be difficult to accept. I'm working with John Harrison's book "Practical Logic and Automated Reasoning" from 2009. It uses OCaml to implement the programs. I've downloaded the OCaml sources from the website. Apparently OCaml has changed significantly from 2009 since the code no longer compiles, spitting out "Alert deprecated" all over the place and simply failing in places. C++ code has a "standard", well, several "standards". When someone asks "Do you know C++" you really need to qualify that question. What you knew about "standard C++" seems to change every 2 years. I recently pulled out my KROPS code, used as the basis for IBM's Expert System FAME. It was written in Common Lisp (on a Symbolics machine). It still runs unmodified despite being written about 40 years ago on hardware and a software stack that no longer exists. Axiom, written in the last century, still compiles and runs. Say what you want about Lisp code, it still is the most portable and long-lasting language I've ever used. Tim
Re: [EXTERNAL] Re: Axiom musings...
No, the name 'Axiom" is used by many different companies. Trademarks only cover infringement "in the same area" (although the Lexus car company sued a diner named Lexus and "won" because the diner couldn't compete against big corporate lawyer money). One company in New Jersey named their language "Axiom" and I keep getting calls from recruiters because that company will pay big bucks to hire an "Axiom Developer". Sigh. I just thought the space one was "over the top". I'd sign up to go to space in a heartbeat. I applied to be an astronaut in the 1990s. NASA wanted someone with at least a Master's degree, a background in Robotics, and less than 5'9" tall. I fit the criteria but never heard back. Tim On 9/25/20, William Sit wrote: > Axiom Space, a Houston-based company, is not related to Axiom the scientific > computation system. Or is it? > > William > > William Sit > Professor Emeritus > Department of Mathematics > The City College of The City University of New York > New York, NY 10031 > homepage: wsit.ccny.cuny.edu > > > From: Axiom-developer > on behalf of > Tim Daly > Sent: Thursday, September 24, 2020 4:26 AM > To: Ricardo Corral C. > Cc: axiom-developer@nongnu.org > Subject: [EXTERNAL] Re: Axiom musings... > > Today's Headline: > > Axiom finalizing agreements for private astronaut mission to space station > > https://urldefense.proofpoint.com/v2/url?u=https-3A__spaceflightnow.com_2020_09_23_axiom-2Dfinalizing-2Dagreements-2Dfor-2Dprivate-2Dastronaut-2Dmission-2Dto-2Dspace-2Dstation_=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8=AvUAZpZ9vnJiQ37yQyMSdNeJQH8qv3HLt5_V1qQ3q2g= > > Wow. I HAVE been busy :-) > > Tim > > > On 9/24/20, Tim Daly wrote: >> Ricardo, >> >> Yes, I'm familar with Sage. Axiom was originally connected >> back around 2006 / 2007. William Stein showed me that it >> runs fine in the latest version. >> >> Unfortunately it doesn't do all of the things Axiom supports. >> >> I will look at Elixer LiveView. Thanks. >> >> Tim >> >> >> On 9/24/20, Ricardo Corral C. wrote: >>> Elixir LiveView offers a nice way to interact with the browser. I’ve been >>> playing rendering OpenAI Atari frames from their Python objects (using >>> erlport), so it seems like a plausible option for interacting with axiom >>> too. Note that sagemath.org already interacts with axiom, so maybe >>> connecting through it serves like a bridge. >>> >>> On Thu 24 Sep 2020 at 0:06 Tim Daly wrote: >>> The new Axiom version needs to have a better user interface. I'm experimenting with a browser front end that has an Axiom editor that runs Axiom in the background. This isn't really a new idea. Maxima has been doing it for years. Using the browser has the advantage of integrating the compiler, interpreter, graphics, and documentation in one interface. I managed to get the editor-in-browser working. Axiom already has a browser connection (book volume 11) designed to replace hyperdoc and working as an interpreter I/O so this editor would be an extension. Since almost all of Axiom is already in hyperlinked PDF files it will be possible to jump directly to related sections in the various books. Tim On 9/23/20, Tim Daly wrote: > Rich Hickey gave a keynote: > https://urldefense.proofpoint.com/v2/url?u=https-3A__www.youtube.com_watch-3Fv-3DoyLBGkS5ICk=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8=oF9rfp-E-CqJ8LCcpq87aURaYtjVP8DwSljlOvjZUFw= > which, like all of Hickey's talks, is worth watching. > > He talks about programs breaking due to things like > library changes. Around minute 30 he started to talk > about why "semantic versioning" (e.g. version 1.2.3) > is meaningless. > > I realized this years ago and changed Axiom to use > the date of the release. It provides the same sort of > "non-information" but it is easy to find in the changelog. > > Tim > > > On 9/5/20, Tim Daly wrote: >> Geometric algebra also affects another "in-process" goal. >> >> I have BLAS and LAPACK in the Axiom sources (volume 10.5). >> >> I've spent some time on the question of changing BLAS to use >> John Gustafson's UNUM representation, which eliminates a lot >> of code because various "standard errors" cannot occur. See >> his book "The End Of Error" >>
Re: [EXTERNAL] Re: Axiom musings...
Axiom Space, a Houston-based company, is not related to Axiom the scientific computation system. Or is it? William William Sit Professor Emeritus Department of Mathematics The City College of The City University of New York New York, NY 10031 homepage: wsit.ccny.cuny.edu From: Axiom-developer on behalf of Tim Daly Sent: Thursday, September 24, 2020 4:26 AM To: Ricardo Corral C. Cc: axiom-developer@nongnu.org Subject: [EXTERNAL] Re: Axiom musings... Today's Headline: Axiom finalizing agreements for private astronaut mission to space station https://urldefense.proofpoint.com/v2/url?u=https-3A__spaceflightnow.com_2020_09_23_axiom-2Dfinalizing-2Dagreements-2Dfor-2Dprivate-2Dastronaut-2Dmission-2Dto-2Dspace-2Dstation_=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8=AvUAZpZ9vnJiQ37yQyMSdNeJQH8qv3HLt5_V1qQ3q2g= Wow. I HAVE been busy :-) Tim On 9/24/20, Tim Daly wrote: > Ricardo, > > Yes, I'm familar with Sage. Axiom was originally connected > back around 2006 / 2007. William Stein showed me that it > runs fine in the latest version. > > Unfortunately it doesn't do all of the things Axiom supports. > > I will look at Elixer LiveView. Thanks. > > Tim > > > On 9/24/20, Ricardo Corral C. wrote: >> Elixir LiveView offers a nice way to interact with the browser. I’ve been >> playing rendering OpenAI Atari frames from their Python objects (using >> erlport), so it seems like a plausible option for interacting with axiom >> too. Note that sagemath.org already interacts with axiom, so maybe >> connecting through it serves like a bridge. >> >> On Thu 24 Sep 2020 at 0:06 Tim Daly wrote: >> >>> The new Axiom version needs to have a better user interface. >>> >>> >>> >>> I'm experimenting with a browser front end that has an Axiom >>> >>> editor that runs Axiom in the background. This isn't really >>> >>> a new idea. Maxima has been doing it for years. >>> >>> >>> >>> Using the browser has the advantage of integrating the >>> >>> compiler, interpreter, graphics, and documentation in one >>> >>> interface. >>> >>> >>> >>> I managed to get the editor-in-browser working. >>> >>> >>> >>> Axiom already has a browser connection (book volume 11) >>> >>> designed to replace hyperdoc and working as an >>> >>> interpreter I/O so this editor would be an extension. >>> >>> >>> >>> Since almost all of Axiom is already in hyperlinked PDF >>> >>> files it will be possible to jump directly to related sections >>> >>> in the various books. >>> >>> >>> >>> Tim >>> >>> >>> >>> >>> >>> >>> >>> On 9/23/20, Tim Daly wrote: >>> >>> > Rich Hickey gave a keynote: >>> >>> > https://urldefense.proofpoint.com/v2/url?u=https-3A__www.youtube.com_watch-3Fv-3DoyLBGkS5ICk=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8=oF9rfp-E-CqJ8LCcpq87aURaYtjVP8DwSljlOvjZUFw= >>> >>> > which, like all of Hickey's talks, is worth watching. >>> >>> > >>> >>> > He talks about programs breaking due to things like >>> >>> > library changes. Around minute 30 he started to talk >>> >>> > about why "semantic versioning" (e.g. version 1.2.3) >>> >>> > is meaningless. >>> >>> > >>> >>> > I realized this years ago and changed Axiom to use >>> >>> > the date of the release. It provides the same sort of >>> >>> > "non-information" but it is easy to find in the changelog. >>> >>> > >>> >>> > Tim >>> >>> > >>> >>> > >>> >>> > On 9/5/20, Tim Daly wrote: >>> >>> >> Geometric algebra also affects another "in-process" goal. >>> >>> >> >>> >>> >> I have BLAS and LAPACK in the Axiom sources (volume 10.5). >>> >>> >> >>> >>> >> I've spent some time on the question of changing BLAS to use >>> >>> >> John Gustafson's UNUM representation, which eliminates a lot >>> >>> >> of code because various "standard errors" cannot occur. See >>> >>> >> his book "The End Of Error" >>> >>> >> >>> https://urldefense.proofpoint.com/v2/url?u=https-3A__www.amazon.com_End-2DError-2DComputing-2DChapman-2DComputational_dp_1482239868=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=HjfsC447T7m29H3fRO5mjUS7vORbNarNjIlj8UKFSH8=yWXuK9IV2lgeUVht6IFybABGGvhsgr0zuqsb6jwFr-4= >>> >>> >> >>> >>> >> But since Geometric algebra is coordinate free, many of the >>> >>> >> computations can be done symbolically and then evalulated >>> >>> >> in final form. >>> >>> >> >>> >>> >> BLAS re-caste in Geometric Algebra means that some of the >>> >>> >> errors, such as roundoff, cannot occur in the symbolic form. >>> >>> >> >>> >>> >> This has the potential to make Axiom's BLAS and LAPACK >>> >>> >> computations faster and more accurate. >>> >>> >> >>> >>> >> Tim >>> >>> >> >>> >>> >> >>> >>> >> On 9/5/20, Tim Daly wrote: >>> >>> >>> I'm in the process of re-architecting Axiom, of course. >>> >>> >>> >>> >>> >>> The primary research effort, as you
Re: [EXTERNAL] Re: Axiom musings...
The question of equality in computation is very different than equality in mathematics and it is basically due to data representations in computation (and for this question, we are not even concerned with equality between two implementations of the same domain but different representations (types), when coercion is needed). As you pointed out, the key question is: "what should be the definition of equality?" even within one single domain and one data representation. Arithmetic in any floating point number system does not satisfy many of the usual laws. For example, a times (b divided by a) is NOT b in such a system unless the system is FP(2,1,c). Here FP(r,p,c) is the floating point system with radix r, precision p, and c for chopping (truncation). The associative laws of addition and multiplication do NOT hold in FP(r,p,c). Strict inequality (less than) between two FP(r,p,c) numbers can be weakened to (less than or equal to) after say adding a third number or multiplied by a positive number. Ref: Pat. H. Sterbenz, Floating Point Computation,Sections 1.6, 1.7. So to prove correctness of implementation for an algorithm, say like taking square roots, will be far more difficult than the same for integers. How can one be convinced that the computation gives the most accurate square root for all inputs in the system FP(r,p,c)? In fact, is there such an algorithm other than one based on case considerations for every number in FP(r,p,c)---you may as well use a lookup table in that case. In the case of polynomial equality between two domains, one can always do a subtraction in the domain of the target of coercion to verify equality. For the specific example you gave, I would agree with Cubical type theory (whatever that is!) that they should be considered equal (unless there is a problem with computing the LCM of denominators of the coefficients). 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 Sent: Saturday, July 25, 2020 5:18 AM To: William Sit Cc: axiom-dev Subject: Re: [EXTERNAL] Re: Axiom musings... The further I get into this game, the harder it becomes. For example, equality. In the easiest case Axiom has propositional equality. That is, the equality function is defined by the type, e.g. for the type Integer, 2 = 2. However, there is also judgmental equality, which would apply at the type level. If floating point numbers match the usual IEEE definition and UNUMs match Gustafson's Type I defintion, is there an equality between the types? Does FLOAT = UNUM? https://urldefense.proofpoint.com/v2/url?u=https-3A__en.wikipedia.org_wiki_Unum-5F-28number-5Fformat-29=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU=Y2MBHvioPEtIrgddTGyKqAMzQ_VeElXxUnvWAYX19HU=tIo8U5fkmzZuvhbq0yoSyRwBb-h2udDjfQfIkCK6qCY= Axiom's coerce provides a (poorly) defined kind of judgmental equality but its not actually defined as an equality at the type level. You can coerce from POLY(FRAC(INT)) to FRAC(POLY(INT)) but are they equal? Cubical type theory would seem to say yes. And don't get me started on the Univalent axiom. There are lots of interesting equality questions. If there is a proof of a program and you can regenerate the program from the proof, are the proof and program equal? Presumably the chap behind the SANE effort will be able to handle both kinds of equality (as well as giving universes for types). But I suspect he's not that clever. On 7/21/20, Tim Daly wrote: >> Yes, I do remember we worked on the "symbolic integer" >> (or "symbolic polynomial", etc.) domains. > > Sadly only the idea survives. > > I spent almost all of my time at that time trying to get a > version of Axiom to bootstrap. Starting Axiom, at the time, > required an already running version of Axiom (the NAG > version) and NAG would not let me distribute their code. > > Building a self-booting version involved (among a lot of > other things) breaking circular definitions in the category > and domain hierarchy. That took several months and all > of my time (much to Baumslag's annoyance). > > That effort also involved re-writing code from Norman's > Lisp back to Common Lisp (much to Norman's annoyance) > > As a result, the free version of Axiom wasn't released until > about 2003 even though I got a copy in 2001. As part of my > employment agreement with CCNY they wouldn't make any > claim on Axiom and I would only work on it in my free time > unless Gilbert said otherwise. My work time was spent as > the Magnus lead developer and open sourcing it. Gilbert > eventually wanted Axiom and asked me to do it for work > also. That's what led to the grant proposal. > > My thoughts on the sub
Re: [EXTERNAL] Re: Axiom musings...
The further I get into this game, the harder it becomes. For example, equality. In the easiest case Axiom has propositional equality. That is, the equality function is defined by the type, e.g. for the type Integer, 2 = 2. However, there is also judgmental equality, which would apply at the type level. If floating point numbers match the usual IEEE definition and UNUMs match Gustafson's Type I defintion, is there an equality between the types? Does FLOAT = UNUM? https://en.wikipedia.org/wiki/Unum_(number_format) Axiom's coerce provides a (poorly) defined kind of judgmental equality but its not actually defined as an equality at the type level. You can coerce from POLY(FRAC(INT)) to FRAC(POLY(INT)) but are they equal? Cubical type theory would seem to say yes. And don't get me started on the Univalent axiom. There are lots of interesting equality questions. If there is a proof of a program and you can regenerate the program from the proof, are the proof and program equal? Presumably the chap behind the SANE effort will be able to handle both kinds of equality (as well as giving universes for types). But I suspect he's not that clever. On 7/21/20, Tim Daly wrote: >> Yes, I do remember we worked on the "symbolic integer" >> (or "symbolic polynomial", etc.) domains. > > Sadly only the idea survives. > > I spent almost all of my time at that time trying to get a > version of Axiom to bootstrap. Starting Axiom, at the time, > required an already running version of Axiom (the NAG > version) and NAG would not let me distribute their code. > > Building a self-booting version involved (among a lot of > other things) breaking circular definitions in the category > and domain hierarchy. That took several months and all > of my time (much to Baumslag's annoyance). > > That effort also involved re-writing code from Norman's > Lisp back to Common Lisp (much to Norman's annoyance) > > As a result, the free version of Axiom wasn't released until > about 2003 even though I got a copy in 2001. As part of my > employment agreement with CCNY they wouldn't make any > claim on Axiom and I would only work on it in my free time > unless Gilbert said otherwise. My work time was spent as > the Magnus lead developer and open sourcing it. Gilbert > eventually wanted Axiom and asked me to do it for work > also. That's what led to the grant proposal. > > My thoughts on the subject of symbolic integers were, as a > consequence, only "paper experiments". I have several > thousand technical papers stacked in my office and library. > The CCNY notes are in there somewhere. Unfortunately, > every time I pick up a pile to search I find other things I > "need to know now" and get lost in that subject. It is like > trying to get a glass of water when the three gorges dam > burst. > > It seems feasible to create a SYMINT Symbolic Integer > domain that used symbols rather than numbers for the > arithmetic, creating a ring that could be used by POLY. > Using SYMINT in SYMFRAC Symboiic Fraction would > provide a field that could be used by POLY. > > The idea is still worth the effort but, as usual, I am deep > into rebuilding Axiom from the ground up. The issues I'm > struggling with now make the bootstrap effort look like a > weekend hack. Bootstrapping took about several months. > The current effort has taken 6 years so far. There is SO > much to know and I am a slow learner. > > This is where I wish I had graduate students :-) > > Tim > > > On 7/21/20, William Sit wrote: >> Dear Tim: >> >> You have expanded on the issues I raised. While you are right that a >> computational algorithm can be proved if the specifications are >> completely >> and precisely coded for the proof systems like Coq. The catch is not the >> precisely part but the completely part. >> >> Yes, I do remember we worked on the "symbolic integer" (or "symbolic >> polynomial", etc.) domains. I think I might have actually some notes and >> ideas and perhaps code, but it would take me more searching than I can do >> now from obsoleted and perhaps non-functional computers. A few days ago, >> I >> was trying to recover tex files from a Raspberry Pi that I used while in >> a >> hotel in China (2015), but nothing (meaning ftp and other transfer >> methods >> or even mailing programs) works because of security. I have also >> forgotten >> all my knowledge on Linux. >> >> Too bad we did not continue that effort. Does such a domain (in any >> computer >> algebra system) exist these days? After all, nearly three decades have >> passed. >> >> William >> >> William Sit >>
Re: [EXTERNAL] Re: Axiom musings...
> Yes, I do remember we worked on the "symbolic integer" > (or "symbolic polynomial", etc.) domains. Sadly only the idea survives. I spent almost all of my time at that time trying to get a version of Axiom to bootstrap. Starting Axiom, at the time, required an already running version of Axiom (the NAG version) and NAG would not let me distribute their code. Building a self-booting version involved (among a lot of other things) breaking circular definitions in the category and domain hierarchy. That took several months and all of my time (much to Baumslag's annoyance). That effort also involved re-writing code from Norman's Lisp back to Common Lisp (much to Norman's annoyance) As a result, the free version of Axiom wasn't released until about 2003 even though I got a copy in 2001. As part of my employment agreement with CCNY they wouldn't make any claim on Axiom and I would only work on it in my free time unless Gilbert said otherwise. My work time was spent as the Magnus lead developer and open sourcing it. Gilbert eventually wanted Axiom and asked me to do it for work also. That's what led to the grant proposal. My thoughts on the subject of symbolic integers were, as a consequence, only "paper experiments". I have several thousand technical papers stacked in my office and library. The CCNY notes are in there somewhere. Unfortunately, every time I pick up a pile to search I find other things I "need to know now" and get lost in that subject. It is like trying to get a glass of water when the three gorges dam burst. It seems feasible to create a SYMINT Symbolic Integer domain that used symbols rather than numbers for the arithmetic, creating a ring that could be used by POLY. Using SYMINT in SYMFRAC Symboiic Fraction would provide a field that could be used by POLY. The idea is still worth the effort but, as usual, I am deep into rebuilding Axiom from the ground up. The issues I'm struggling with now make the bootstrap effort look like a weekend hack. Bootstrapping took about several months. The current effort has taken 6 years so far. There is SO much to know and I am a slow learner. This is where I wish I had graduate students :-) Tim On 7/21/20, William Sit wrote: > Dear Tim: > > You have expanded on the issues I raised. While you are right that a > computational algorithm can be proved if the specifications are completely > and precisely coded for the proof systems like Coq. The catch is not the > precisely part but the completely part. > > Yes, I do remember we worked on the "symbolic integer" (or "symbolic > polynomial", etc.) domains. I think I might have actually some notes and > ideas and perhaps code, but it would take me more searching than I can do > now from obsoleted and perhaps non-functional computers. A few days ago, I > was trying to recover tex files from a Raspberry Pi that I used while in a > hotel in China (2015), but nothing (meaning ftp and other transfer methods > or even mailing programs) works because of security. I have also forgotten > all my knowledge on Linux. > > Too bad we did not continue that effort. Does such a domain (in any computer > algebra system) exist these days? After all, nearly three decades have > passed. > > 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 > Sent: Monday, July 20, 2020 4:44 PM > To: William Sit > Cc: axiom-dev > Subject: Re: [EXTERNAL] Re: Axiom musings... > >> So there are two kinds of algorithms, one that is purely mathematical >> and one that is computational, the latter including a particular (class >> of) >> data representation(s) (perhaps even the computer language and >> system of the implementation). It is proofs for the latter type of >> algorithms that is lacking. > > There are ,as you point out, several kinds of proofs to consider. > > One is the proof of the algorithm. An example is Buchberger's > Groebner Basis algorithm which was proven in Coq: > https://urldefense.proofpoint.com/v2/url?u=https-3A__www.ricam.oeaw.ac.at_specsem_srs_groeb_download_coq-2Dlinz.pdf=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU=qJcX0eywVfbeyLAuiHayc0VdCrprfGa-v65dRgMKAuE=48_B3YVCzXBpYUWOgsuSY0mMrrZd9SpQzWVZki-c6d4= > > The Coq proof establishes that the formal algorithm is correct. > > Even in proof one runs into limits of what can be proved. For example, > if the convergence is non-uniform one can, at best, do a proof that > assumes bounds on the non-uniform behavior. So this isn't strictly > a computer algorithm issue. > >> Since data represen
Re: [EXTERNAL] Re: Axiom musings...
Dear Tim: You have expanded on the issues I raised. While you are right that a computational algorithm can be proved if the specifications are completely and precisely coded for the proof systems like Coq. The catch is not the precisely part but the completely part. Yes, I do remember we worked on the "symbolic integer" (or "symbolic polynomial", etc.) domains. I think I might have actually some notes and ideas and perhaps code, but it would take me more searching than I can do now from obsoleted and perhaps non-functional computers. A few days ago, I was trying to recover tex files from a Raspberry Pi that I used while in a hotel in China (2015), but nothing (meaning ftp and other transfer methods or even mailing programs) works because of security. I have also forgotten all my knowledge on Linux. Too bad we did not continue that effort. Does such a domain (in any computer algebra system) exist these days? After all, nearly three decades have passed. 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 Sent: Monday, July 20, 2020 4:44 PM To: William Sit Cc: axiom-dev Subject: Re: [EXTERNAL] Re: Axiom musings... > So there are two kinds of algorithms, one that is purely mathematical > and one that is computational, the latter including a particular (class of) > data representation(s) (perhaps even the computer language and > system of the implementation). It is proofs for the latter type of > algorithms that is lacking. There are ,as you point out, several kinds of proofs to consider. One is the proof of the algorithm. An example is Buchberger's Groebner Basis algorithm which was proven in Coq: https://urldefense.proofpoint.com/v2/url?u=https-3A__www.ricam.oeaw.ac.at_specsem_srs_groeb_download_coq-2Dlinz.pdf=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU=qJcX0eywVfbeyLAuiHayc0VdCrprfGa-v65dRgMKAuE=48_B3YVCzXBpYUWOgsuSY0mMrrZd9SpQzWVZki-c6d4= The Coq proof establishes that the formal algorithm is correct. Even in proof one runs into limits of what can be proved. For example, if the convergence is non-uniform one can, at best, do a proof that assumes bounds on the non-uniform behavior. So this isn't strictly a computer algorithm issue. > Since data representations (like REP in Axiom) are built recursively, > a computational algorithm (in the sense above) for Groebner basis > may have to be designed to take care of just a few of the ways > integers can be represented. Axiom is built with that in mind (that's > where type theory comes in), but I bet no one SPECIFIES their > computational algorithms with the limitations of data representation > in mind, much less proves the algorithm anew for each new > representation. If you remember, while we were both at CCNY, I worked on a grant project to construct a "symbolic integer" domain so that computations could occur over non-numeric integers. The symbolic form did not have a numeric limitation. Unfortunatly the current Axiom has no way to support such a domain. I'm glad you brought this up. I will have to give some thought to representing and computing with symbolic integers again. > So if a computation of a Groebner basis halts > because of an intermediate LCM computation (say of two integer > coefficients), should we consider the implementation as proven > correct? What if the overflow condition was not detected and the > computation continues? Indeed, since there may be different > implementations of the integer domain, we must be sure that > every implementation of the LCM algorithm handles overflows > correctly AND specified in the documentation. Establishing that the algorithm is correct (e.g Groebner) is clearly in the proof side of computational math . Establishing that there is an implementation of Groebner is clearly in the computer algebra side of computational math. The game is to unite the two. Such a proof becomes a PART of the specification of a program that implements the algorithm, such as in Axiom. The definitions and axioms of the proof have to be put into the system both at the category and domain levels. They need to be available at the implementation code. On the other hand, there are non-logical 'axioms' of categories and domains, such as limits to the size of a floating point number. One could have many FLOAT domains, such as Gustafson's UNUMs. https://urldefense.proofpoint.com/v2/url?u=http-3A__www.johngustafson.net_pdfs_BeatingFloatingPoint.pdf=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=pGhsxwcTvR8Ap4fl9FnvlW2_HcwzcFuj51GHaBlmYIU=qJcX0eywVfbeyLAuiHayc0VdCrprfGa-v65dRgMKAuE=wrah9xCIC0aDYjDhQgMxrQb_NM6HKkKp_QbW91Vx4Y4= There are non-logical limits to the implementation, such as intermediate exp
Re: [EXTERNAL] Re: Axiom musings...
ion is not the same as the > abstract mathematical objects because there are finite bounds on the > representation. Take for example, an algorithm to compute the LCM of two > integers. The LCM can cause overflow and not be representable. Of course, > you can change the data representation to have "infinite precision", but > that would still be bounded by actual physical memory of the machine. The > careful programmer of the LCM algorithm would add throws and catches to > handle the "error",but the implementation will have to add code that is not > considered in the theoretical LCM algorithm (unless the LCM algorithm is > meant for bounded integers of a fixed data representation and not abstract > integers). So there are two kinds of algorithms, one that is purely > mathematical and one that is computational, the latter including a > particular (class of) data representation(s) (perhaps even the computer > language and system of the implementation). It is proofs for the latter type > of algorithms that is lacking. Since data representations (like REP in > Axiom) are built recursively, a computational algorithm (in the sense above) > for Groebner basis may have to be designed to take care of just a few of the > ways integers can be represented. Axiom is built with that in mind (that's > where type theory comes in), but I bet no one SPECIFIES their computational > algorithms with the limitations of data representation in mind, much less > proves the algorithm anew for each new representation. So if a computation > of a Groebner basis halts because of an intermediate LCM computation (say of > two integer coefficients), should we consider the implementation as proven > correct? What if the overflow condition was not detected and the computation > continues? Indeed, since there may be different implementations of the > integer domain, we must be sure that every implementation of the LCM > algorithm handles overflows correctly AND specified in the documentation. > > I am sure I am just being ignorant to pose these questions, because they > must have been considered and perhaps solved. In that case, please ignore > them and just tell me so. > > 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 > Sent: Sunday, July 19, 2020 5:33 PM > To: William Sit > Cc: axiom-dev > Subject: Re: [EXTERNAL] Re: Axiom musings... > > There are several "problems" with proving programs correct that > I don't quite know how to solve, or even approach. But that's the > fun of "research", right? > > For the data representation question I've been looking at types. > I took 10 courses at CMU. I am eyebrow deep in type theory. > I'm looking at category theory and homotopy type theory. So > far I haven't seen anyone looking at the data problem. Most of > the focus is on strict code typing. > > There is an old MIT course by Abelson and Sussman "Structure > and Interpretation of Computer Programs" (SICP). They rewrite > data as programs which, in Lisp, is trivial to do, Dan Friedman > seems to have some interesting ideas too. > > All of Axiom's SANE types are now CLOS objects which gives > two benefits. First, they can be inherited. But second, they > are basically Lisp data structures with associated code. > > I'm thinking of associating "data axioms" with the representation > (REP) object of a domain as well as with the functions. > > For example, DenavitHartenbergMatrix encodes 4x4 matrices > used in graphics and robotics. They are 4x4 matrices where > the upper left 3x3 encodes rotations, the right column encodes > translations, and the lower row includes scaling, skewing, etc. > > (As an aside, DHMATRIX matrices have an associated > Jacobian which encodes the dynamics in things like robots. > Since I'm also programming a robot I'm tempted to work on > extending the domain with related functions... but, as > Hamming said, new algebra code isn't "the most important > problem in computational mathematics"). > > Axioms associated with the REP can assume that they are > 4x4, that they can be inverted, that they have a "space" of > rotations, etc. The axioms provide "facts" known to be true > about the REP. (I also need to think about a "specification" > for the REP but I'm not there yet). > > Since every category and domain is a CLOS data structure > the DHMATRIX data structure inherits REP axioms from its > inheritance graph (e.g. SQMATRIX axioms). But DHMATRIX > adds domain-specific REP axioms (as w
Re: [EXTERNAL] Re: Axiom musings...
Hi Tim: Perhaps I did not make myself clear in the short comment. What I wanted to say is that a data representation is not the same as the abstract mathematical objects because there are finite bounds on the representation. Take for example, an algorithm to compute the LCM of two integers. The LCM can cause overflow and not be representable. Of course, you can change the data representation to have "infinite precision", but that would still be bounded by actual physical memory of the machine. The careful programmer of the LCM algorithm would add throws and catches to handle the "error",but the implementation will have to add code that is not considered in the theoretical LCM algorithm (unless the LCM algorithm is meant for bounded integers of a fixed data representation and not abstract integers). So there are two kinds of algorithms, one that is purely mathematical and one that is computational, the latter including a particular (class of) data representation(s) (perhaps even the computer language and system of the implementation). It is proofs for the latter type of algorithms that is lacking. Since data representations (like REP in Axiom) are built recursively, a computational algorithm (in the sense above) for Groebner basis may have to be designed to take care of just a few of the ways integers can be represented. Axiom is built with that in mind (that's where type theory comes in), but I bet no one SPECIFIES their computational algorithms with the limitations of data representation in mind, much less proves the algorithm anew for each new representation. So if a computation of a Groebner basis halts because of an intermediate LCM computation (say of two integer coefficients), should we consider the implementation as proven correct? What if the overflow condition was not detected and the computation continues? Indeed, since there may be different implementations of the integer domain, we must be sure that every implementation of the LCM algorithm handles overflows correctly AND specified in the documentation. I am sure I am just being ignorant to pose these questions, because they must have been considered and perhaps solved. In that case, please ignore them and just tell me so. 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 Sent: Sunday, July 19, 2020 5:33 PM To: William Sit Cc: axiom-dev Subject: Re: [EXTERNAL] Re: Axiom musings... There are several "problems" with proving programs correct that I don't quite know how to solve, or even approach. But that's the fun of "research", right? For the data representation question I've been looking at types. I took 10 courses at CMU. I am eyebrow deep in type theory. I'm looking at category theory and homotopy type theory. So far I haven't seen anyone looking at the data problem. Most of the focus is on strict code typing. There is an old MIT course by Abelson and Sussman "Structure and Interpretation of Computer Programs" (SICP). They rewrite data as programs which, in Lisp, is trivial to do, Dan Friedman seems to have some interesting ideas too. All of Axiom's SANE types are now CLOS objects which gives two benefits. First, they can be inherited. But second, they are basically Lisp data structures with associated code. I'm thinking of associating "data axioms" with the representation (REP) object of a domain as well as with the functions. For example, DenavitHartenbergMatrix encodes 4x4 matrices used in graphics and robotics. They are 4x4 matrices where the upper left 3x3 encodes rotations, the right column encodes translations, and the lower row includes scaling, skewing, etc. (As an aside, DHMATRIX matrices have an associated Jacobian which encodes the dynamics in things like robots. Since I'm also programming a robot I'm tempted to work on extending the domain with related functions... but, as Hamming said, new algebra code isn't "the most important problem in computational mathematics"). Axioms associated with the REP can assume that they are 4x4, that they can be inverted, that they have a "space" of rotations, etc. The axioms provide "facts" known to be true about the REP. (I also need to think about a "specification" for the REP but I'm not there yet). Since every category and domain is a CLOS data structure the DHMATRIX data structure inherits REP axioms from its inheritance graph (e.g. SQMATRIX axioms). But DHMATRIX adds domain-specific REP axioms (as well as domain-specific function axioms). Thus a DHMATRIX rotate function can base its proof on the fact that it only affects the upper 3x3 and lives in a space of rotations, all of which can be assumed by the proof. If I use the SICP "trick" of representing data as code I can
Re: [EXTERNAL] Re: Axiom musings...
There are several "problems" with proving programs correct that I don't quite know how to solve, or even approach. But that's the fun of "research", right? For the data representation question I've been looking at types. I took 10 courses at CMU. I am eyebrow deep in type theory. I'm looking at category theory and homotopy type theory. So far I haven't seen anyone looking at the data problem. Most of the focus is on strict code typing. There is an old MIT course by Abelson and Sussman "Structure and Interpretation of Computer Programs" (SICP). They rewrite data as programs which, in Lisp, is trivial to do, Dan Friedman seems to have some interesting ideas too. All of Axiom's SANE types are now CLOS objects which gives two benefits. First, they can be inherited. But second, they are basically Lisp data structures with associated code. I'm thinking of associating "data axioms" with the representation (REP) object of a domain as well as with the functions. For example, DenavitHartenbergMatrix encodes 4x4 matrices used in graphics and robotics. They are 4x4 matrices where the upper left 3x3 encodes rotations, the right column encodes translations, and the lower row includes scaling, skewing, etc. (As an aside, DHMATRIX matrices have an associated Jacobian which encodes the dynamics in things like robots. Since I'm also programming a robot I'm tempted to work on extending the domain with related functions... but, as Hamming said, new algebra code isn't "the most important problem in computational mathematics"). Axioms associated with the REP can assume that they are 4x4, that they can be inverted, that they have a "space" of rotations, etc. The axioms provide "facts" known to be true about the REP. (I also need to think about a "specification" for the REP but I'm not there yet). Since every category and domain is a CLOS data structure the DHMATRIX data structure inherits REP axioms from its inheritance graph (e.g. SQMATRIX axioms). But DHMATRIX adds domain-specific REP axioms (as well as domain-specific function axioms). Thus a DHMATRIX rotate function can base its proof on the fact that it only affects the upper 3x3 and lives in a space of rotations, all of which can be assumed by the proof. If I use the SICP "trick" of representing data as code I can "expand" the data as part of the program proof. It is all Omphaloskepsis (navel gazing) at this point though. I'm still writing the new SANE compiler (which is wildly different from the compiler course I taught). I did give a talk at Notre Dame but I haven't attempted to publish. All of my work shows up in literate programming Axiom books on github. (https://github.com/daly/PDFS) It is all pretty pointless since nobody cares about computer algebra, proving math programs correct, or Axiom itself. Wolfram is taking up all the oxygen in the discussions. But I have to say, this research is great fun. It reminds me of the Scratchpad days, although I miss the give-and-take of the group. It is hard to recreate my role as the dumbest guy in the room when I'm stuck here by myself :-) Hope you and your family are safe and healthy. Tim PS. I think we should redefine the "Hamming Distance" as the distance between an idea and its implementation. On 7/19/20, William Sit wrote: > Hi Tim: > > Glad to hear from you now and then, promoting and working towards your ideas > and ideals. > > >>We need proven algorithms. > > Just one short comment: it is often possible to prove algorithms (that is, > providing the theoretical foundation for the algorithm), but it is much > harder to prove that an implementation of the algorithm is correct. As you > well know, the distinction lies in that implementation involves data > representations whereas proofs of algorithms normally ignore them. > Introducing (finite) data representations means introducing boundary > situations that a programmer implementing an algorithm must deal with. So > perhaps what we need to prove should include the correctness of > implementations (to the bare metal, as you often say) and we should have a > different set of analytic tools that can deal with the correctness (or > completeness) of data representations. Of course, these tools must also be > proven with the same rigor since behind every program is an algorithm. > > William > > William Sit > Professor Emeritus > Department of Mathematics > The City College of The City University of New York > New York, NY 10031 > homepage: wsit.ccny.cuny.edu > > > From: Axiom-developer > on behalf of > Tim Daly > Sent: Saturday, July 18, 2020 6:28 PM > To: axiom-dev; Tim Daly > Subject: [EXTERNAL] Re: Axiom musings... > > Richard Hamming gave a great talk. "You and Your Research" >
Re: [EXTERNAL] Re: Axiom musings...
Hi Tim: Glad to hear from you now and then, promoting and working towards your ideas and ideals. >>We need proven algorithms. Just one short comment: it is often possible to prove algorithms (that is, providing the theoretical foundation for the algorithm), but it is much harder to prove that an implementation of the algorithm is correct. As you well know, the distinction lies in that implementation involves data representations whereas proofs of algorithms normally ignore them. Introducing (finite) data representations means introducing boundary situations that a programmer implementing an algorithm must deal with. So perhaps what we need to prove should include the correctness of implementations (to the bare metal, as you often say) and we should have a different set of analytic tools that can deal with the correctness (or completeness) of data representations. Of course, these tools must also be proven with the same rigor since behind every program is an algorithm. William William Sit Professor Emeritus Department of Mathematics The City College of The City University of New York New York, NY 10031 homepage: wsit.ccny.cuny.edu From: Axiom-developer on behalf of Tim Daly Sent: Saturday, July 18, 2020 6:28 PM To: axiom-dev; Tim Daly Subject: [EXTERNAL] Re: Axiom musings... Richard Hamming gave a great talk. "You and Your Research" https://urldefense.proofpoint.com/v2/url?u=https-3A__www.youtube.com_watch-3Fv-3Da1zDuOPkMSw=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=_2V6ryqOIDfXNZePX0kmp-2428hMSBYbz5fq8bDzgkQ=kSXlFiPNCbYVZvoZ62OUVd_40kcVviTxSKF3vNNtm0U= His big question is: "What is the most important problem in your field and why aren't you working on it?" To my mind, the most important problem in the field of computational mathematics is grounding computer algebra in proofs. Computer mathematical algorithms that "maybe, possibly, give correct answers sometimes" is a problem. Indeed, for computer algebra, it is the most important problem. We need proven algorithms. New algorithms, better graphics, better documentation, are all "nice to have" but, as Hamming would say, they are not "the most important problem". Tim On 7/2/20, Tim Daly wrote: > Time for another update. > > The latest Intel processors, available only to data centers > so far, have a built-in FPGA. This allows you to design > your own circuits and have them loaded "on the fly", > running in parallel with the CPU. > > I bought a Lattice ICEstick FPGA development board. For > the first time there are open source tools that support it so > it is a great test bench for ideas and development. It is a > USB drive so it can be easily ported to any PC. > (https://urldefense.proofpoint.com/v2/url?u=https-3A__www.latticesemi.com_products_developmentboardsandkits_icestick=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=_2V6ryqOIDfXNZePX0kmp-2428hMSBYbz5fq8bDzgkQ=QxcJcE1BdIMqDbutQz2HFhAAAymG-QswIjRao_YTwz4= > ) > > I also bought a large Intel Cyclone FPGA development board. > (https://urldefense.proofpoint.com/v2/url?u=http-3A__www.terasic.com.tw_cgi-2Dbin_page_archive.pl-3FLanguage-3DEnglish-26No-3D836=DwIFaQ=4NmamNZG3KTnUCoC6InoLJ6KV1tbVKrkZXHRwtIMGmo=qW9SUYRDo6sWEVPpx7wwWYZ79PdSWMRxNZvTih0Bkxc=_2V6ryqOIDfXNZePX0kmp-2428hMSBYbz5fq8bDzgkQ=3wW6BueAeyVTQi0xGqoeE7xIA5EREDmvQR4fPw5zAXo= > ) > which has 2 embedded ARM processors. Unfortunately > the tools (which are freely available) are not open source. > It has sufficient size and power to do anything. > > > I've got 2 threads of work in progress, both of which > involve FPGAs (Field Programmable Gate Arrays). > > Thread 1 > > The first thread involves proving programs correct. Once > a proof has been made it is rather easier to check the proof. > If code is shipped with a proof, the proof can be loaded into > an FPGA running a proof-checker which verifies the program > in parallel with running the code on the CPU. > > I am researching the question of writing a proof checker that > runs on an FPGA, thus verifying the code "down to the metal". > The Lean proof checker is the current target. > > The idea is to make "Oracle" algorithms that, because they > are proven correct and verified at runtime, can be trusted > by other mathematical software (e.g. Lean, Coq, Agda) > when used in proofs. > > Thread 2 > > > The second thread involves arithmetic. Axiom currently ships > with numeric routines (BLAS and LAPACK, see bookvol10.5). > These routines have a known set of numeric failures such as > cancellation, underflow, and scaling. > > John Gustafson has designed a 'unum' numeric format that can > eliminate many of these errors. (See > Gustafson, John "The End of Error" CRC Press 2015 >
