Axiom musings ... proof specificity

An interesting idea is what I'd call "proof specificity". The motivation is to prove that certain classes of bugs cannot occur. Or, more generally, that certain classes of behavior cannot occur. At a very low level there could be a proof that the stack size is bounded. A slightly higher level

Re: Axiom musings ... runtime computation of first-class dependent types

Tim, Thanks for your reply, lots to think about in this subject isn't there. Like you I'm attempting the daunting (but interesting) path of trying to understand this subject better. Dependent types allow functions to exist in the type definition. The functions can be executed "at run time".

Re: Axiom musings ... runtime computation of first-class dependent types

Martin, >In this series of videos Robert Harper gives an provocative take on >these subjects: >https://www.youtube.com/watch?v=LE0SSLizYUI I watched Harper's videos years ago. I will revisit them. If you haven't seen them I highly recommend them.

Re: Axiom musings ... runtime computation of first-class dependent types

Tim In this series of videos Robert Harper gives an provocative take on these subjects: https://www.youtube.com/watch?v=LE0SSLizYUI At about 37 min into this video he says: "what is true has unbounded quantifier complexity whereas any formalism is always relentlessly recursively

Axiom musings ... runtime computation of first-class dependent types

Well, SANE is certainly turning into a journey. When we look at the idea of first-class dependent types as implemented in languages like Agda and Idris we find what I call "peano types". For example, Fin is a type of "finite numbers", usually defined as data Fin : Nat -> Type where FZ : Fin (S

Axiom musings ... SANE and long term viability

I've been living with Axiom's code now since the 1980s, a portion of which I've authored or, at least, rewritten. The code was written by some truly clever people (and I'm not one of them). The parser, written by Bill Burge, uses a "zipper" technique. It is quite clever and absolutely opaque.

Re: Axiom musings ... Hamming and SANE

... [snip] ... I've been scratching at Wittgenstein, the Vienna Circle, and Godel. It got me thinking about the notion of Type hierarchies and the current view of Type theory, specifically its use to eliminate paradox. Which leads my thoughts to the current fad of types and functional

Axiom musings ... Hamming and SANE

... [snip] ... I guess that's where we differ. Axiom is a piece of research software. Axiom was never intended to be a product. IBM gave us two choices. Either find someone to market it (NAG) or throw it away. FOSS software did not exist at that time and we were not allowed to work on it in any

Re: Axiom musings...

Full support for general, first-class dependent types requires some changes to the Axiom design. That implies some language design questions. Given that mathematics is such a general subject with a lot of "local" notation and ideas (witness logical judgment notation) careful thought is needed to

Re: Axiom musings...

I have a separate thread of research on Self-Replicating Systems (ref: Kinematics of Self Reproducing Machines http://www.molecularassembler.com/KSRM.htm) which led to watching "Strange Dreams of Stranger Loops" by Will Byrd https://www.youtube.com/watch?v=AffW-7ika0E Will referenced a PhD

Re: Axiom musings...

So the current struggle involves the categories in Axiom. The categories and domains constructed using categories are dependent types. When are dependent types "equal"? Well, hu, that depends on the arguments to the constructor. But in order to decide(?) equality we have to evaluate the

Re: Axiom musings...

"Birthing Computational Mathematics" The Axiom SANE project is difficult at a very fundamental level. The title "SANE" was chosen due to the various words found in a thesuarus... "rational", "coherent", "judicious" and "sound". These are very high level, amorphous ideas. But so is the design of

Re: Axiom musings...

I have tried to maintain a list of names of people who have helped Axiom, going all the way back to the pre-Scratchpad days. The names are listed at the beginning of each book. I also maintain a bibliography of publications I've read or that have had an indirect influence on Axiom. Credit is "the

Re: Axiom musings...

Greg Wilson asked "How Reliable is Scientific Software?" https://neverworkintheory.org/2021/09/25/how-reliable-is-scientific-software.html which is a really interesting read. For example" [Hatton1994], is now a quarter of a century old, but its conclusions are still fresh. The authors fed the

Re: Axiom musings...

I should note that the lastest board I've just unboxed (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD). What makes it interesting is that it contains 2 hard core processors and an FPGA, connected by 9 paths for communication. The processors can be run independently so there is the possibility

Re: Axiom musings...

I'm familiar with most of the traditional approaches like Theorema. The bibliography contains most of the more interesting sources. [0] There is a difference between traditional approaches to connecting computer algebra and proofs and my approach. Proving an algorithm, like the GCD, in Axiom is

Re: Axiom musings...

= REVIEW (Axiom on WSL2 Windows) So the steps to run Axiom from a Windows desktop 1 Windows) install XMing on Windows for X11 server http://www.straightrunning.com/XmingNotes/ 2 WSL2) Install Axiom in WSL2 sudo apt install axiom 3 WSL2) modify

Re: Axiom musings...

A great deal of thought is directed toward making the SANE version of Axiom as flexible as possible, decoupling mechanism from theory. An interesting publication by Brian Cantwell Smith [0], "Reflection and Semantics in LISP" seems to contain interesting ideas related to our goal. Of particular

Re: Axiom musings...

Having spent time playing with hardware it is perfectly clear that future computational mathematics efforts need to adapt to using parallel processing. I've spent a fair bit of time thinking about structuring Axiom to be parallel. Most past efforts have tried to focus on making a particular

Re: Axiom musings...

Axiom is based on first-class dependent types. Deciding when two types are equivalent may involve computation. See Christiansen, David Thrane "Checking Dependent Types with Normalization by Evaluation" (2019) This puts an interesting constraint on building types. The constructed types has to

Re: Axiom musings...

It is interesting that programmer's eyes and expectations adapt to the tools they use. For instance, I use emacs and expect to work directly in files and multiple buffers. When I try to use one of the many IDE tools I find they tend to "get in the way". I already know or can quickly find whatever

Re: Axiom musings...

The systems I use have the interesting property of "Living within the compiler". Lisp, Forth, Emacs, and other systems that present themselves through the Read-Eval-Print-Loop (REPL) allow the ability to deeply interact with the system, shaping it to your need. My current thread of study is

Re: Axiom musings...

The Axiom SANE compiler / interpreter has a few design points. 1) It needs to mix interpreted and compiled code in the same function. SANE allows dynamic construction of code as well as dynamic type construction at runtime. Both of these can occur in a runtime object. So there is potentially a

Re: Axiom musings...

I've worked hard to make Axiom depend on almost no other tools so that it would not get caught by "code rot" of libraries. However, I'm also trying to make the new SANE version much easier to understand and debug.To that end I've been experimenting with some ideas. It should be possible to view

Re: Axiom musings...

Also of interest is the talk "The Unreasonable Effectiveness of Dynamic Typing for Practical Programs" https://vimeo.com/74354480 which questions whether static typing really has any benefit. Tim On 1/19/21, Tim Daly wrote: > Peter Naur wrote an article of interest: >

Re: Axiom musings...

Peter Naur wrote an article of interest: http://pages.cs.wisc.edu/~remzi/Naur.pdf In particular, it mirrors my notion that Axiom needs to embrace literate programming so that the "theory of the problem" is presented as well as the "theory of the solution". I quote the introduction: This

Re: Axiom musings...

Another thought is that Axiom is "not fully factored". There is a logic and category theory concept called "the carrier". In Axiom terms, this is the Rep aka the representation. Axiom bundles the representation with the domain, which is reasonable. However, representations are likely data

Re: Axiom musings...

One of the struggles of working with first-class dependent types is that they can be created "on the fly". Ideally, when used, the type information can be "factored out" to yield a specialized version that is more efficient. The idea is best described in a book, called Partial Evaluation, which

Re: Axiom musings...

It's been a long, slow effort to "get up to speed" (or more accurately "a slow crawl") on the various subjects one needs to know to work on "computational mathematics" aka SANE. A reading knowledge of a lot of areas is needed, including things like abstract algebra (to understand Axiom's

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

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

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

Re: Axiom musings...

Robert Harper's "Holy Trinity" of Computer Science (aka "Computational Trinitarianism") Proof Theory (Logic) / \ /\ Category Theory Type Theory (Mathematics)

Re: Axiom musings...

HILL CLIMBING I really encourage you to read the slides: Vladimir Voevodsky. Univalent foundations, March 2014. Presentation at IAS,http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf The mathematical references likely won't make sense but the most important point of

Re: Axiom musings...

I just ran across an interesting example about the difference between testing and proving (not that I need to be convinced). http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf (page 10): On day one, our mathematician finds out using a formal computation software that

Re: Axiom musings...

Axiom, as it was released to me long ago, is being overtaken by current technology. I'm taking an MIT course on "Underactuated Robots" [0] (I spent a large portion of my life doing robotics). The instructor is using Jupyter notebooks to illustrate control algorithms. He is doing computation and

Re: Axiom musings...

The current mental struggle involves properly re-constructing Axiom so Category Theory (e.g. objects, morphisms, identity, and composition) is respected between the domains. Done properly, this should make resolving type coercion and conversion less ad-hoc. This is especially important when

Re: Axiom musings...

Another area that is taking a great deal of time and effort is choosing a code architecture that has a solid background in research. Axiom used CLU and Group Theory as two scaffolds to guide design choices, making it possible to argue whether and where a domain should be structured and where it

Re: Axiom musings...

A great deal of thought has gone into the representation of functions in the SANE version. It is important that a function lives within an environment. There are no "stand alone" functions. Given a function its environment contains the representation which itself is a function type with accessor

Re: Axiom musings...

I'm writing a book on the history of Axiom. As part of that effort I'm reviewing all of the emails posted to the mailing list. I came across this posting by Scott Morrison, the author of the interpreter: Date: Thu, 3 Nov 2005 08:34:55 -0800 From: Scott Morrison To: list Subject: Re: BAD tim

Re: Axiom musings...

Hill Climbing Almost every possible step along the path to creating the SANE version of Axiom involves a LOT of hill climbing, by that I mean a LOT to learn to get started. Axiom was built with a scaffold of group theory which makes it easier to reason about and understand. Going forward we

Re: Axiom musings...

My apologies. I reacted poorly to what I interpreted as a criticism of the developers of Scratchpad. I consider them among the most clever and intelligent people I've ever met. I was lucky to work with them. Tim

Axiom musings...

(https://groups.google.com/g/fricas-devel/c/lF4w9MduSVg) -- There is quality called "cohesion" or "conceptual -- integrity" meaning that parts of system follow common -- design and compose into coherent whole. I could list -- rather long list of design choices made in Axiom time -- that I am not

Re: [EXTERNAL] Re: Axiom musings...

__ > 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 astronau

Re: [EXTERNAL] Re: Axiom musings...

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

Re: Axiom musings...

Today's Headline: Axiom finalizing agreements for private astronaut mission to space station https://spaceflightnow.com/2020/09/23/axiom-finalizing-agreements-for-private-astronaut-mission-to-space-station/ Wow. I HAVE been busy :-) Tim On 9/24/20, Tim Daly wrote: > Ricardo, > > Yes, I'm

Re: Axiom musings...

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

Re: Axiom musings...

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

Re: Axiom musings...

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,

Re: Axiom musings...

Rich Hickey gave a keynote: https://www.youtube.com/watch?v=oyLBGkS5ICk 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

Re: Axiom musings...

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.

Re: Axiom musings...

I'm in the process of re-architecting Axiom, of course. The primary research effort, as you know, is incorporating proof technology. But in the process of re-architecting there are more things to consider. Two of them are "front and center" at the moment. One concern is "Geometric Algebra". See

Re: Axiom musings...

A briliant essay: In exactly the same way a small change in axioms (of which we cannot be completely sure) is capable, generally speaking, of leading to completely different conclusions than those that are obtained from theorems which have been deduced from the accepted axioms. The longer and

Re: Axiom musings...

Mark, You're right, of course. The problem is too large. So what. is the plan to achieve a research result? There are 3 major restrictions on the effort (so far). First, the focus is on the GCD in NonNegativeInteger. Volume 13 is basically a collection of published thoughts by various authors

Re: Axiom musings...

page: 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

Re: [EXTERNAL] Re: Axiom musings...

y.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, th

Re: [EXTERNAL] Re: Axiom musings...

ch 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 o

Re: [EXTERNAL] Re: Axiom musings...

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 > > _________

Re: [EXTERNAL] Re: Axiom musings...

__ 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 o

Re: [EXTERNAL] Re: Axiom musings...

ps 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 > > ___

Re: [EXTERNAL] Re: Axiom musings...

k 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 qu

Re: [EXTERNAL] Re: Axiom musings...

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 D

Re: [EXTERNAL] Re: Axiom musings...

ny.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.youtu

Re: Axiom musings...

Richard Hamming gave a great talk. "You and Your Research" https://www.youtube.com/watch?v=a1zDuOPkMSw 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

Re: Axiom musings...

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

Re: Axiom musings...

WHY PROVE AXIOM CORRECT (SANE)? Historically, Axiom credits CLU, the Cluster language by Barbara Liskov, with the essential ideas behind the Spad language. Barbara gave a talk (a partial transcript below) that gives the rational behind the ``where clause'' used by Spad. She talks about the

Re: Axiom musings...

I've spent entirely too much time studing the legal issues of free and open source software. There are copyright, trademark, and intellectual property laws. I have read several books, listened to lectures, and read papers on the subject. I've spoken to lawyers about it. I've even been required, by

Re: Axiom musings...

I've pushed the lastest version of Axiom. The plan, followed so far, is to push once a month on the 7th. After some chat room interactions it was brought home again that the proof world really does not seem to like the idea of proving programs correct. And, given that it was is of the main Axiom

Re: Axiom musings...

As a mathematician, it is difficult to use a system like Axiom, mostly because it keeps muttering about Types. If you're not familiar with type theory (most mathematicians aren't) then it seems pointless and painful. So Axiom has a steep learning curve. As a mathematician with an algorithmic

Re: Axiom musings...

When Axiom Sane is paired with a proof checker (e.g. with Lean) there is a certain amount of verification that is involved. Axiom will provide proofs (presumably validated by Lean) for its algorithms. Ideally, when a computation is requested from Lean for a GCD, the result as well as a proof of

Re: Axiom musings...

Trusted Kernel... all the way to the metal. While building a trusted computer algebra system, the SANE version of Axiom, I've been looking at questions of trust at all levels. One of the key tenets (the de Bruijn principle) calls for a trusted kernel through which all other computations must

Re: Axiom musings...

Tim, Would this also be compatible with 'propositions as types' as in Idris and various proof assistants? That is, could you have both Curry–Howard and Carette-Farmer? I ask this because types (and constructors for types) could also be inherited by categories in the way you describe. So an

Re: Axiom musings...

Progress in happening on the new Sane Axiom compiler. Recently I've been musing about methods to insert axioms into categories so they could be inherited like signatures. At the moment I've been thinking about adding axioms in the same way that signatures are written, adding them to the

Re: Axiom musings...

I've been reading Stephen Kell's (Univ of Kent https://www.cs.kent.ac.uk/people/staff/srk21/) on Seven deadly sins of talking about “types” https://www.cs.kent.ac.uk/people/staff/srk21//blog/2014/10/07/ He raised an interesting idea toward the end of the essay that type-checking could be done

Re: Axiom musings...

The Axiom Sane compiler is being "shaped by the hammer blows of reality", to coin a phrase. There are many goals. One of the primary goals is creating a compiler that can be understood, maintained, and modified. So the latest changes involved adding multiple index files. These are documentation

Re: Axiom musings...

The underlying technology to use for building such an algebra library is documented in the paper " Building on the Diamonds between Theories: Theory Presentation Combinators" http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [which will also be on the arxiv by Monday, and has been

Re: Axiom musings...

I'm still undecided about accepting unicode on input as opposed to latex-style input (e.g. \pi vs the unicode pi character). The logic syntax would really benefit from using things like \forall as a unicode character on input. It makes the math I/O much prettier but it makes parsing much harder.

Re: Axiom musings...

The new Sane compiler is also being tested with the Fricas algebra code. The compiler knows about the language but does not depend on the algebra library (so far). It should be possible, by design, to load different algebra towers. In particular, one idea is to support the "tiny theories" algebra

Re: Axiom musings...

The current design and code base (in bookvol15) supports multiple back ends. One will clearly be a common lisp. Another possible design choice is to target the GNU GCC intermediate representation, making Axiom "just another front-end language" supported by GCC. The current intermediate

Axiom musings...

Jason Gross and Adam Chlipala ("Parsing Parses") developed a dependently typed general parser for context free grammar in Coq. They used the parser to prove its own completeness. Unfortunately Spad is not a context-free grammar. But it is an intersting thought exercise to consider an "Axiom on

Axiom musings....

The latest Sane book is uploaded, a work in progress. The major development is the start of parsing. The internal data structures are the target and they have already been mostly developed as the system is being written "middle-out". That is, the intermediate representation was the first thing

Re: [Axiom-developer] Axiom musings...

Peter Naur addressed the primary issue of literate programming: http://pages.cs.wisc.edu/~remzi/Naur.pdf A "programming theory" is the ability to reason about a program in some abstract sense. Given a question about some theory of types (e.g. linear logic), you can close your eyes and decide if

Re: [Axiom-developer] Axiom musings...

As you might expect, the new Axiom Sane effort is fully literate, developed solely as a literate program. One of the subgoals is to write a page per day. This can involve explaining code. But it also involves explaining various ideas that are related to the effort. The current topic is a section

[Axiom-developer] Axiom musings...

I have been programming for 50 years. There is always the personal challenge of "keeping up with the edge". In the wire-board and punched card days it was the ability to choose the optimal sort for your data (almost everything involved sorting). Then came the cpu optimizations... write