Re: Axiom musings...

--Apple-Mail-18CBE148-0FFC-47D9-9D95-5D7EFE73CB6B
Content-Transfer-Encoding: quoted-printable
Content-Type: text/plain;
	charset=utf-8

The setup of a spreadsheet is similar to the design of some prototype based p=
rogramming languages. I have recently been learning about the Self programmi=
ng language, a descendant of Smalltalk, which uses prototypes rather than cl=
asses. This creates a more dynamic environment.

Like Smalltalk, development is done using a virtual machine with a programmi=
ng environment. The objects in the Self environment can be configured using d=
irect manipulation to define behavior and inheritance.

https://selflanguage.org/

It should be possible to develop a similar prototype system based in lisp, i=
f it has not been done already.

On Mar 23, 2022, at 1:53, Tim Daly <[email protected]> wrote:

> I have a deep interest in self-modifying programs. These are
> trivial to create in lisp. The question is how to structure a computer
> algebra program so it could be dynamically modified but still=20
> well-structured. This is especially important since the user can
> create new logical types at runtime.
>=20
> One innovation, which I have never seen anywhere, is to structure
> the program in a spreadsheet fashion. Spreadsheets cells can
> reference other spreadsheet cells. Spreadsheets have a well-defined
> evaluation method. This is equivalent to a form of object-oriented
> programming where each cell is an object and has a well-defined
> inheritance hierarchy through other cells. Simple manipulation
> allows insertion, deletion, or modification of these chains at any time.
>=20
> So by structuring a computer algebra program like a spreadsheet
> I am able to dynamically adjust a program to fit the problem to be
> solved, track which cells are needed, and optimize the program.
>=20
> Spreadsheets do this naturally but I'm unaware of any non-spreadsheet
> program that relies on that organization.
>=20
> Tim
>=20
>=20
> On Sun, Mar 13, 2022 at 4:01 AM Tim Daly <[email protected]> wrote:
> Axiom has an awkward 'attributes' category structure.
>=20
> In the SANE version it is clear that these attributes are much
> closer to logic 'definitions'. As a result one of the changes
> is to create a new 'category'-type structure for definitions.
> There will be a new keyword, like the category keyword,
> 'definition'.
>=20
> Tim
>=20
>=20
> On Fri, Mar 11, 2022 at 9:46 AM Tim Daly <[email protected]> wrote:
> The github lockout continues...=20
>=20
> I'm spending some time adding examples to source code.
>=20
> Any function can have ++X comments added. These will
> appear as examples when the function is )display For example,
> in PermutationGroup there is a function 'strongGenerators'
> defined as:
>=20
>   strongGenerators : % -> L PERM S
>     ++ strongGenerators(gp) returns strong generators for
>     ++ the group gp.
>     ++
>     ++X S:List(Integer) :=3D [1,2,3,4]
>     ++X G :=3D symmetricGroup(S)
>     ++X strongGenerators(G)
>=20
>=20
>=20
> Later, in the interpreter we see:
>=20
>=20
>=20
>=20
> )d op strongGenerators
>=20
>   There is one exposed function called strongGenerators :
>       [1] PermutationGroup(D2) -> List(Permutation(D2)) from
>                PermutationGroup(D2)
>                  if D2 has SETCAT
>=20
>   Examples of strongGenerators from PermutationGroup
>  =20
>   S:List(Integer) :=3D [1,2,3,4]
>   G :=3D symmetricGroup(S)
>   strongGenerators(G)
>=20
>=20
>=20
>=20
> This will show a working example for functions that the
> user can copy and use. It is especially useful to show how
> to construct working arguments.
>=20
> These "example" functions are run at build time when
> the make command looks like
>     make TESTSET=3Dalltests
>=20
> I hope to add this documentation to all Axiom functions.
>=20
> In addition, the plan is to add these function calls to the
> usual test documentation. That means that all of these examples
> will be run and show their output in the final distribution
> (mnt/ubuntu/doc/src/input/*.dvi files) so the user can view
> the expected output.
>=20
> Tim
>=20
>=20
>=20
>=20
> On Fri, Feb 25, 2022 at 6:05 PM Tim Daly <[email protected]> wrote:
> It turns out that creating SPAD-looking output is trivial=20
> in Common Lisp. Each class can have a custom print
> routine so signatures and ++ comments can each be
> printed with their own format.
>=20
> To ensure that I maintain compatibility I'll be printing
> the categories and domains so they look like SPAD code,
> at least until I get the proof technology integrated. I will
> probably specialize the proof printers to look like the
> original LEAN proof syntax.
>=20
> Internally, however, it will all be Common Lisp.
>=20
> Common Lisp makes so many desirable features so easy.
> It is possible to trace dynamically at any level. One could
> even write a trace that showed how Axiom arrived at the
> solution. Any domain could have special case output syntax
> without affecting any other domain so one could write a
> tree-like output for proofs. Using greek characters is trivial
> so the input and output notation is more mathematical.
>=20
> Tim
>=20
>=20
> On Thu, Feb 24, 2022 at 10:24 AM Tim Daly <[email protected]> wrote:
> Axiom's SPAD code compiles to Common Lisp.
> The AKCL version of Common Lisp compiles to C.
> Three languages and 2 compilers is a lot to maintain.
> Further, there are very few people able to write SPAD
> and even fewer people able to maintain it.
>=20
> I've decided that the SANE version of Axiom will be=20
> implemented in pure Common Lisp. I've outlined Axiom's
> category / type hierarchy in the Common Lisp Object
> System (CLOS). I am now experimenting with re-writing
> the functions into Common Lisp.
>=20
> This will have several long-term effects. It simplifies
> the implementation issues. SPAD code blocks a lot of
> actions and optimizations that Common Lisp provides.
> The Common Lisp language has many more people
> who can read, modify, and maintain code. It provides for
> interoperability with other Common Lisp projects with
> no effort. Common Lisp is an international standard
> which ensures that the code will continue to run.
>=20
> The input / output mathematics will remain the same.
> Indeed, with the new generalizations for first-class
> dependent types it will be more general.
>=20
> This is a big change, similar to eliminating BOOT code
> and moving to Literate Programming. This will provide a
> better platform for future research work. Current research
> is focused on merging Axiom's computer algebra mathematics
> with Lean's proof language. The goal is to create a system for
>  "computational mathematics".
>=20
> Research is the whole point of Axiom.
>=20
> Tim
>=20
>=20
>=20
> On Sat, Jan 22, 2022 at 9:16 PM Tim Daly <[email protected]> wrote:
> I can't stress enough how important it is to listen to Hamming's talk
> https://www.youtube.com/watch?v=3Da1zDuOPkMSw
>=20
> Axiom will begin to die the day I stop working on it.
>=20
> However, proving Axiom correct "down to the metal", is fundamental.
> It will merge computer algebra and logic, spawning years of new
> research.
>=20
> Work on fundamental problems.
>=20
> Tim
>=20
>=20
> On Thu, Dec 30, 2021 at 6:46 PM Tim Daly <[email protected]> wrote:
> One of the interesting questions when obtaining a result
> is "what functions were called and what was their return value?"
> Otherwise known as the "show your work" idea.
>=20
> There is an idea called the "writer monad" [0], usually=20
> implemented to facilitate logging. We can exploit this
> idea to provide "show your work" capability. Each function
> can provide this information inside the monad enabling the
> question to be answered at any time.
>=20
> For those unfamiliar with the monad idea, the best explanation
> I've found is this video [1].
>=20
> Tim
>=20
> [0] Deriving the writer monad from first principles
> https://williamyaoh.com/posts/2020-07-26-deriving-writer-monad.html
>=20
> [1] The Absolute Best Intro to Monads for Software Engineers
> https://www.youtube.com/watch?v=3DC2w45qRc3aU
>=20
> On Mon, Dec 13, 2021 at 12:30 AM Tim Daly <[email protected]> wrote:
> ...(snip)...
>=20
> Common Lisp has an "open compiler". That allows the ability
> to deeply modify compiler behavior using compiler macros
> and macros in general. CLOS takes advantage of this to add
> typed behavior into the compiler in a way that ALLOWS strict
> typing such as found in constructive type theory and ML.
> Judgments, ala Crary, are front-and-center.
>=20
> Whether you USE the discipline afforded is the real question.
>=20
> Indeed, the Axiom research struggle is essentially one of how
> to have a disciplined use of first-class dependent types. The
> struggle raises issues of, for example, compiling a dependent
> type whose argument is recursive in the compiled type. Since
> the new type is first-class it can be constructed at what you
> improperly call "run-time". However, it appears that the recursive
> type may have to call the compiler at each recursion to generate
> the next step since in some cases it cannot generate "closed code".
>=20
> I am embedding proofs (in LEAN language) into the type
> hierarchy so that theorems, which depend on the type hierarchy,
> are correctly inherited. The compiler has to check the proofs of functions=

> at compile time using these. Hacking up nonsense just won't cut it. Think
> of the problem of embedding LEAN proofs in ML or ML in LEAN.
> (Actually, Jeremy Avigad might find that research interesting.)
>=20
> So Matrix(3,3,Float) has inverses (assuming Float is a
> field (cough)). The type inherits this theorem and proofs of
> functions can use this. But Matrix(3,4,Integer) does not have
> inverses so the proofs cannot use this. The type hierarchy has
> to ensure that the proper theorems get inherited.
>=20
> Making proof technology work at compile time is hard.
> (Worse yet, LEAN is a moving target. Sigh.)
>=20
>=20
>=20
> On Thu, Nov 25, 2021 at 9:43 AM Tim Daly <[email protected]> wrote:
>=20
> As you know I've been re-architecting Axiom to use first class
> dependent types and proving the algorithms correct. For example,
> the GCD of natural numbers or the GCD of polynomials.
>=20
> The idea involves "boxing up" the proof with the algorithm (aka
> proof carrying code) in the ELF file (under a crypto hash so it
> can't be changed).
>=20
> Once the code is running on the CPU, the proof is run in parallel
> on the field programmable gate array (FPGA). Intel data center
> servers have CPUs with built-in FPGAs these days.
>=20
> There is a bit of a disconnect, though. The GCD code is compiled
> machine code but the proof is LEAN-level.
>=20
> What would be ideal is if the compiler not only compiled the GCD
> code to machine code, it also compiled the proof to "machine code".
> That is, for each machine instruction, the FPGA proof checker
> would ensure that the proof was not violated at the individual
> instruction level.
>=20
> What does it mean to "compile a proof to the machine code level"?
>=20
> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
> To quote from the article [0]:
>=20
>    We begin with a simple proof checker, call it A, which is short
>    enough to verify by the ``social process'' of mathematics -- and
>   more recently with a theorem prover for a more expressive logic.
>=20
>    We then develop a series of increasingly powerful proof checkers,
>   call the B, C, D, and so on. We show each of these programs only
>    accepts the same formulas as A, using A to verify B, and B to verify
>    C, and so on. Then, since we trust A, and A says B is trustworthy, we
>    can trust B. Then, since we trust B, and B says C is trustworthy, we
>    can trust C.=20
>=20
> This gives a technique for "compiling the proof" down the the machine
> code level. Ideally, the compiler would have judgments for each step of
> the compilation so that each compile step has a justification. I don't
> know of any compiler that does this yet. (References welcome).
>=20
> At the machine code level, there are techniques that would allow
> the FPGA proof to "step in sequence" with the executing code.
> Some work has been done on using "Hoare Logic for Realistically
> Modelled Machine Code" (paper attached, Myre07a.pdf),
> "Decompilation into Logic -- Improved (Myre12a.pdf).
>=20
> So the game is to construct a GCD over some type (Nats, Polys, etc.
> Axiom has 22), compile the dependent type GCD to machine code.
> In parallel, the proof of the code is compiled to machine code. The
> pair is sent to the CPU/FPGA and, while the algorithm runs, the FPGA
> ensures the proof is not violated, instruction by instruction.
>=20
> (I'm ignoring machine architecture issues such pipelining, out-of-order,
> branch prediction, and other machine-level things to ponder. I'm looking
> at the RISC-V Verilog details by various people to understand better but
> it is still a "misty fog" for me.)
>=20
> The result is proven code "down to the metal".
>=20
> Tim
>=20
>=20
>=20
> [0] https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/inde=
x-seo.php/ACL2____MILAWA
>=20
> On Thu, Nov 25, 2021 at 6:05 AM Tim Daly <[email protected]> wrote:
>=20
> As you know I've been re-architecting Axiom to use first class
> dependent types and proving the algorithms correct. For example,
> the GCD of natural numbers or the GCD of polynomials.
>=20
> The idea involves "boxing up" the proof with the algorithm (aka
> proof carrying code) in the ELF file (under a crypto hash so it
> can't be changed).
>=20
> Once the code is running on the CPU, the proof is run in parallel
> on the field programmable gate array (FPGA). Intel data center
> servers have CPUs with built-in FPGAs these days.
>=20
> There is a bit of a disconnect, though. The GCD code is compiled
> machine code but the proof is LEAN-level.
>=20
> What would be ideal is if the compiler not only compiled the GCD
> code to machine code, it also compiled the proof to "machine code".
> That is, for each machine instruction, the FPGA proof checker
> would ensure that the proof was not violated at the individual
> instruction level.
>=20
> What does it mean to "compile a proof to the machine code level"?
>=20
> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
> To quote from the article [0]:
>=20
>    We begin with a simple proof checker, call it A, which is short
>    enough to verify by the ``social process'' of mathematics -- and
>   more recently with a theorem prover for a more expressive logic.
>=20
>    We then develop a series of increasingly powerful proof checkers,
>   call the B, C, D, and so on. We show each of these programs only
>    accepts the same formulas as A, using A to verify B, and B to verify
>    C, and so on. Then, since we trust A, and A says B is trustworthy, we
>    can trust B. Then, since we trust B, and B says C is trustworthy, we
>    can trust C.=20
>=20
> This gives a technique for "compiling the proof" down the the machine
> code level. Ideally, the compiler would have judgments for each step of
> the compilation so that each compile step has a justification. I don't
> know of any compiler that does this yet. (References welcome).
>=20
> At the machine code level, there are techniques that would allow
> the FPGA proof to "step in sequence" with the executing code.
> Some work has been done on using "Hoare Logic for Realistically
> Modelled Machine Code" (paper attached, Myre07a.pdf),
> "Decompilation into Logic -- Improved (Myre12a.pdf).
>=20
> So the game is to construct a GCD over some type (Nats, Polys, etc.
> Axiom has 22), compile the dependent type GCD to machine code.
> In parallel, the proof of the code is compiled to machine code. The
> pair is sent to the CPU/FPGA and, while the algorithm runs, the FPGA
> ensures the proof is not violated, instruction by instruction.
>=20
> (I'm ignoring machine architecture issues such pipelining, out-of-order,
> branch prediction, and other machine-level things to ponder. I'm looking
> at the RISC-V Verilog details by various people to understand better but
> it is still a "misty fog" for me.)
>=20
> The result is proven code "down to the metal".
>=20
> Tim
>=20
>=20
>=20
> [0] https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/inde=
x-seo.php/ACL2____MILAWA
>=20
> On Sat, Nov 13, 2021 at 5:28 PM Tim Daly <[email protected]> wrote:
> Full support for general, first-class dependent types requires
> some changes to the Axiom design. That implies some language
> design questions.
>=20
> 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 design a language that is able to
> handle a wide range.
>=20
> Normally language design is a two-level process. The language
> designer creates a language and then an implementation. Various
> design choices affect the final language.
>=20
> There is "The Metaobject Protocol" (MOP)
> https://www.amazon.com/Art-Metaobject-Protocol-Gregor-Kiczales/dp/02626107=
44
> which encourages a three-level process. The language designer=20
> works at a Metalevel to design a family of languages, then the
> language specializations, then the implementation. A MOP design
> allows the language user to optimize the language to their problem.
>=20
> A simple paper on the subject is "Metaobject Protocols"
> https://users.cs.duke.edu/~vahdat/ps/mop.pdf
>=20
> Tim
>=20
>=20
> On Mon, Oct 25, 2021 at 7:42 PM Tim Daly <[email protected]> wrote:
> I have a separate thread of research on Self-Replicating Systems
> (ref: Kinematics of Self Reproducing Machines
> http://www.molecularassembler.com/KSRM.htm)
>=20
> which led to watching "Strange Dreams of Stranger Loops" by Will Byrd
> https://www.youtube.com/watch?v=3DAffW-7ika0E
>=20
> Will referenced a PhD Thesis by Jon Doyle
> "A Model for Deliberation, Action, and Introspection"
>=20
> I also read the thesis by J.C.G. Sturdy
> "A Lisp through the Looking Glass"
>=20
> Self-replication requires the ability to manipulate your own
> representation in such a way that changes to that representation
> will change behavior.
>=20
> This leads to two thoughts in the SANE research.
>=20
> First, "Declarative Representation". That is, most of the things
> about the representation should be declarative rather than
> procedural. Applying this idea as much as possible makes it
> easier to understand and manipulate.
>=20
> Second, "Explicit Call Stack". Function calls form an implicit
> call stack. This can usually be displayed in a running lisp system.
> However, having the call stack explicitly available would mean
> that a system could "introspect" at the first-class level.
>=20
> These two ideas would make it easy, for example, to let the
> system "show the work". One of the normal complaints is that
> a system presents an answer but there is no way to know how
> that answer was derived. These two ideas make it possible to
> understand, display, and even post-answer manipulate
> the intermediate steps.
>=20
> Having the intermediate steps also allows proofs to be
> inserted in a step-by-step fashion. This aids the effort to
> have proofs run in parallel with computation at the hardware
> level.
>=20
> Tim
>=20
>=20
>=20
>=20
>=20
>=20
> On Thu, Oct 21, 2021 at 9:50 AM Tim Daly <[email protected]> wrote:
> So the current struggle involves the categories in Axiom.
>=20
> The categories and domains constructed using categories
> are dependent types. When are dependent types "equal"?
> Well, hummmm, that depends on the arguments to the
> constructor.
>=20
> But in order to decide(?) equality we have to evaluate
> the arguments (which themselves can be dependent types).
> Indeed, we may, and in general, we must evaluate the=20
> arguments at compile time (well, "construction time" as
> there isn't really a compiler / interpreter separation anymore.)
>=20
> That raises the question of what "equality" means. This
> is not simply a "set equality" relation. It falls into the
> infinite-groupoid of homotopy type theory. In general
> it appears that deciding category / domain equivalence
> might force us to climb the type hierarchy.
>=20
> Beyond that, there is the question of "which proof"
> applies to the resulting object. Proofs depend on their
> assumptions which might be different for different
> constructions. As yet I have no clue how to "index"
> proofs based on their assumptions, nor how to=20
> connect these assumptions to the groupoid structure.
>=20
> My brain hurts.
>=20
> Tim
>=20
>=20
> On Mon, Oct 18, 2021 at 2:00 AM Tim Daly <[email protected]> wrote:
> "Birthing Computational Mathematics"
>=20
> 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".
>=20
> These are very high level, amorphous ideas. But so is
> the design of SANE. Breaking away from tradition in
> computer algebra, type theory, and proof assistants
> is very difficult. Ideas tend to fall into standard jargon
> which limits both the frame of thinking (e.g. dependent
> types) and the content (e.g. notation).
>=20
> Questioning both frame and content is very difficult.
> It is hard to even recognize when they are accepted
> "by default" rather than "by choice". What does the idea
> "power tools" mean in a primitive, hand labor culture?
>=20
> Christopher Alexander [0] addresses this problem in
> a lot of his writing. Specifically, in his book "Notes on
> the Synthesis of Form", in his chapter 5 "The Selfconsious
> Process", he addresses this problem directly. This is a
> "must read" book.
>=20
> Unlike building design and contruction, however, there
> are almost no constraints to use as guides. Alexander
> quotes Plato's Phaedrus:
>=20
>   "First, the taking in of scattered particulars under
>    one Idea, so that everyone understands what is being
>    talked about ... Second, the separation of the Idea
>    into parts, by dividing it at the joints, as nature
>    directs, not breaking any limb in half as a bad=20
>    carver might."
>=20
> Lisp, which has been called "clay for the mind" can
> build virtually anything that can be thought. The=20
> "joints" are also "of one's choosing" so one is
> both carver and "nature".
>=20
> Clearly the problem is no longer "the tools".
> *I* am the problem constraining the solution.
> Birthing this "new thing" is slow, difficult, and
> uncertain at best.
>=20
> Tim
>=20
> [0] Alexander, Christopher "Notes on the Synthesis
> of Form" Harvard University Press 1964=20
> ISBN 0-674-62751-2
>=20
>=20
> On Sun, Oct 10, 2021 at 4:40 PM Tim Daly <[email protected]> wrote:
> Re: writing a paper... I'm not connected to Academia
> so anything I'd write would never make it into print.
>=20
> "Language level parsing" is still a long way off. The talk
> by Guy Steele [2] highlights some of the problems we
> currently face using mathematical metanotation.
>=20
> For example, a professor I know at CCNY (City College
> of New York) didn't understand Platzer's "funny
> fraction notation" (proof judgements) despite being
> an expert in Platzer's differential equations area.
>=20
> Notation matters and is not widely common.
>=20
> I spoke to Professor Black (in LTI) about using natural
> language in the limited task of a human-robot cooperation
> in changing a car tire.  I looked at the current machine
> learning efforts. They are no where near anything but
> toy systems, taking too long to train and are too fragile.
>=20
> Instead I ended up using a combination of AIML [3]
> (Artificial Intelligence Markup Language), the ALICE
> Chatbot [4], Forgy's OPS5 rule based program [5],
> and Fahlman's SCONE [6] knowledge base. It was
> much less fragile in my limited domain problem.
>=20
> I have no idea how to extend any system to deal with
> even undergraduate mathematics parsing.
>=20
> Nor do I have any idea how I would embed LEAN
> knowledge into a SCONE database, although I
> think the combination would be useful and interesting.
>=20
> I do believe that, in the limited area of computational
> mathematics, we are capable of building robust, proven
> systems that are quite general and extensible. As you
> might have guessed I've given it a lot of thought over
> the years :-)
>=20
> A mathematical language seems to need >6 components
>=20
> 1) We need some sort of a specification language, possibly
> somewhat 'propositional' that introduces the assumptions
> you mentioned (ref. your discussion of numbers being
> abstract and ref. your discussion of relevant choice of
> assumptions related to a problem).
>=20
> This is starting to show up in the hardware area (e.g.
> Lamport's TLC[0])
>=20
> Of course, specifications relate to proving programs
> and, as you recall, I got a cold reception from the
> LEAN community about using LEAN for program proofs.
>=20
> 2) We need "scaffolding". That is, we need a theory
> that can be reduced to some implementable form
> that provides concept-level structure.
>=20
> Axiom uses group theory for this. Axiom's "category"
> structure has "Category" things like Ring. Claiming
> to be a Ring brings in a lot of "Signatures" of functions
> you have to implement to properly be a Ring.
>=20
> Scaffolding provides a firm mathematical basis for
> design. It provides a link between the concept of a
> Ring and the expectations you can assume when
> you claim your "Domain" "is a Ring". Category
> theory might provide similar structural scaffolding
> (eventually... I'm still working on that thought garden)
>=20
> LEAN ought to have a textbook(s?) that structures
> the world around some form of mathematics. It isn't
> sufficient to say "undergraduate math" is the goal.
> There needs to be some coherent organization so
> people can bring ideas like Group Theory to the
> organization. Which brings me to ...
>=20
> 3) We need "spreading". That is, we need to take
> the various definitions and theorems in LEAN and
> place them in their proper place in the scaffold.
>=20
> For example, the Ring category needs the definitions
> and theorems for a Ring included in the code for the
> Ring category. Similarly, the Commutative category
> needs the definitions and theorems that underlie
> "commutative" included in the code.
>=20
> That way, when you claim to be a "Commutative Ring"
> you get both sets of definitions and theorems. That is,
> the inheritance mechanism will collect up all of the
> definitions and theorems and make them available
> for proofs.
>=20
> I am looking at LEAN's definitions and theorems with
> an eye to "spreading" them into the group scaffold of
> Axiom.
>=20
> 4) We need "carriers" (Axiom calls them representations,
> aka "REP"). REPs allow data structures to be defined
> independent of the implementation.
>=20
> For example, Axiom can construct Polynomials that
> have their coefficients in various forms of representation.
> You can define "dense" (all coefficients in a list),
> "sparse" (only non-zero coefficients), "recursive", etc.
>=20
> A "dense polynomial" and a "sparse polynomial" work
> exactly the same way as far as the user is concerned.
> They both implement the same set of functions. There
> is only a difference of representation for efficiency and
> this only affects the implementation of the functions,
> not their use.
>=20
> Axiom "got this wrong" because it didn't sufficiently
> separate the REP from the "Domain". I plan to fix this.
>=20
> LEAN ought to have a "data structures" subtree that
> has all of the definitions and axioms for all of the
> existing data structures (e.g. Red-Black trees). This
> would be a good undergraduate project.
>=20
> 5) We need "Domains" (in Axiom speak). That is, we
> need a box that holds all of the functions that implement
> a "Domain". For example, a "Polynomial Domain" would
> hold all of the functions for manipulating polynomials
> (e.g polynomial multiplication). The "Domain" box
> is a dependent type that:
>=20
>   A) has an argument list of "Categories" that this "Domain"
>       box inherits. Thus, the "Integer Domain" inherits
>       the definitions and axioms from "Commutative"
>=20
>      Functions in the "Domain" box can now assume
>      and use the properties of being commutative. Proofs
>      of functions in this domain can use the definitions
>      and proofs about being commutative.
>=20
>   B) contains an argument that specifies the "REP"
>        (aka, the carrier). That way you get all of the
>        functions associated with the data structure
>       available for use in the implementation.
>=20
>       Functions in the Domain box can use all of
>       the definitions and axioms about the representation
>       (e.g. NonNegativeIntegers are always positive)
>=20
>   C) contains local "spread" definitions and axioms
>        that can be used in function proofs.
>=20
>       For example, a "Square Matrix" domain would
>       have local axioms that state that the matrix is
>       always square. Thus, functions in that box could
>       use these additional definitions and axioms in
>       function proofs.
>=20
>   D) contains local state. A "Square Matrix" domain
>        would be constructed as a dependent type that
>        specified the size of the square (e.g. a 2x2
>        matrix would have '2' as a dependent parameter.
>=20
>   E) contains implementations of inherited functions.
>=20
>        A "Category" could have a signature for a GCD
>        function and the "Category" could have a default
>        implementation. However, the "Domain" could
>        have a locally more efficient implementation which
>        overrides the inherited implementation.
>=20
>       Axiom has about 20 GCD implementations that
>       differ locally from the default in the category. They
>       use properties known locally to be more efficient.
>=20
>   F) contains local function signatures.
>=20
>       A "Domain" gives the user more and more unique
>       functions. The signature have associated
>       "pre- and post- conditions" that can be used
>       as assumptions in the function proofs.
>=20
>       Some of the user-available functions are only
>       visible if the dependent type would allow them
>       to exist. For example, a general Matrix domain
>       would have fewer user functions that a Square
>       Matrix domain.
>=20
>       In addition, local "helper" functions need their
>       own signatures that are not user visible.
>=20
>   G) the function implementation for each signature.
>=20
>        This is obviously where all the magic happens
>=20
>   H) the proof of each function.
>=20
>        This is where I'm using LEAN.
>=20
>        Every function has a proof. That proof can use
>        all of the definitions and axioms inherited from
>        the "Category", "Representation", the "Domain
>        Local", and the signature pre- and post-
>        conditions.
>=20
>    I) literature links. Algorithms must contain a link
>       to at least one literature reference. Of course,
>       since everything I do is a Literate Program
>       this is obviously required. Knuth said so :-)
>=20
>=20
> LEAN ought to have "books" or "pamphlets" that
> bring together all of this information for a domain
> such as Square Matrices. That way a user can
> find all of the related ideas, available functions,
> and their corresponding proofs in one place.
>=20
> 6) User level presentation.
>=20
>     This is where the systems can differ significantly.
>     Axiom and LEAN both have GCD but they use
>     that for different purposes.
>=20
>     I'm trying to connect LEAN's GCD and Axiom's GCD
>     so there is a "computational mathematics" idea that
>     allows the user to connect proofs and implementations.
>=20
> 7) Trust
>=20
> Unlike everything else, computational mathematics
> can have proven code that gives various guarantees.
>=20
> I have been working on this aspect for a while.
> I refer to it as trust "down to the metal" The idea is
> that a proof of the GCD function and the implementation
> of the GCD function get packaged into the ELF format.
> (proof carrying code). When the GCD algorithm executes
> on the CPU, the GCD proof is run through the LEAN
> proof checker on an FPGA in parallel.
>=20
> (I just recently got a PYNQ Xilinx board [1] with a CPU
> and FPGA together. I'm trying to implement the LEAN
> proof checker on the FPGA).
>=20
> We are on the cusp of a revolution in computational
> mathematics. But the two pillars (proof and computer
> algebra) need to get know each other.
>=20
> Tim
>=20
>=20
>=20
> [0] Lamport, Leslie "Chapter on TLA+"
> in "Software Specification Methods"
> https://www.springer.com/gp/book/9781852333539
> (I no longer have CMU library access or I'd send you
> the book PDF)
>=20
> [1] https://www.tul.com.tw/productspynq-z2.html
>=20
> [2] https://www.youtube.com/watch?v=3DdCuZkaaou0Q
>=20
> [3] "ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE"
> https://arxiv.org/pdf/1307.3091.pdf
>=20
> [4] ALICE Chatbot
> http://www.scielo.org.mx/pdf/cys/v19n4/1405-5546-cys-19-04-00625.pdf
>=20
> [5] OPS5 User Manual
> https://kilthub.cmu.edu/articles/journal_contribution/OPS5_user_s_manual/6=
608090/1
>=20
> [6] Scott Fahlman "SCONE"
> http://www.cs.cmu.edu/~sef/scone/
>=20
> On 9/27/21, Tim Daly <[email protected]> wrote:
> > 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 coin of the realm". It is easy to share and wrong
> > to ignore. It is especially damaging to those in Academia who
> > are affected by credit and citations in publications.
> >
> > Apparently I'm not the only person who feels that way. The ACM
> > Turing award seems to have ignored a lot of work:
> >
> > Scientific Integrity, the 2021 Turing Lecture, and the 2018 Turing
> > Award for Deep Learning
> > https://people.idsia.ch/~juergen/scientific-integrity-turing-award-deep-=
learning.html
> >
> > I worked on an AI problem at IBM Research called Ketazolam.
> > (https://en.wikipedia.org/wiki/Ketazolam). The idea was to recognize
> > and associated 3D chemical drawings with their drug counterparts.
> > I used Rumelhart, and McClelland's books. These books contained
> > quite a few ideas that seem to be "new and innovative" among the
> > machine learning crowd... but the books are from 1987. I don't believe
> > I've seen these books mentioned in any recent bibliography.
> > https://mitpress.mit.edu/books/parallel-distributed-processing-volume-1
> >
> >
> >
> >
> > On 9/27/21, Tim Daly <[email protected]> wrote:
> >> Greg Wilson asked "How Reliable is Scientific Software?"
> >> https://neverworkintheory.org/2021/09/25/how-reliable-is-scientific-sof=
tware.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 same data into nine commercial
> >> geophysical software packages and compared the results; they found
> >> that, "numerical disagreement grows at around the rate of 1% in
> >> average absolute difference per 4000 fines of implemented code, and,
> >> even worse, the nature of the disagreement is nonrandom" (i.e., the
> >> authors of different packages make similar mistakes).
> >>
> >>
> >> On 9/26/21, Tim Daly <[email protected]> wrote:
> >>> 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 of a parallel
> >>> version of some Axiom algorithms (assuming I had
> >>> the time, which I don't).
> >>>
> >>> Previously either the hard (physical) processor was
> >>> separate from the FPGA with minimal communication
> >>> or the soft core processor had to be created in the FPGA
> >>> and was much slower.
> >>>
> >>> Now the two have been combined in a single chip.
> >>> That means that my effort to run a proof checker on
> >>> the FPGA and the algorithm on the CPU just got to
> >>> the point where coordination is much easier.
> >>>
> >>> Now all I have to do is figure out how to program this
> >>> beast.
> >>>
> >>> There is no such thing as a simple job.
> >>>
> >>> Tim
> >>>
> >>>
> >>> On 9/26/21, Tim Daly <[email protected]> wrote:
> >>>> 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 hard.
> >>>> There are many GCDs (e.g. NNI vs POLY) and there
> >>>> are theorems and proofs passed at runtime in the
> >>>> arguments of the newly constructed domains. This
> >>>> involves a lot of dependent type theory and issues of
> >>>> compile time / runtime argument evaluation. The issues
> >>>> that arise are difficult and still being debated in the type
> >>>> theory community.
> >>>>
> >>>> I am putting the definitions, theorems, and proofs (DTP)
> >>>> directly into the category/domain hierarchy. Each category
> >>>> will have the DTP specific to it. That way a commutative
> >>>> domain will inherit a commutative theorem and a
> >>>> non-commutative domain will not.
> >>>>
> >>>> Each domain will have additional DTPs associated with
> >>>> the domain (e.g. NNI vs Integer) as well as any DTPs
> >>>> it inherits from the category hierarchy. Functions in the
> >>>> domain will have associated DTPs.
> >>>>
> >>>> A function to be proven will then inherit all of the relevant
> >>>> DTPs. The proof will be attached to the function and
> >>>> both will be sent to the hardware (proof-carrying code).
> >>>>
> >>>> The proof checker, running on a field programmable
> >>>> gate array (FPGA), will be checked at runtime in
> >>>> parallel with the algorithm running on the CPU
> >>>> (aka "trust down to the metal"). (Note that Intel
> >>>> and AMD have built CPU/FPGA combined chips,
> >>>> currently only available in the cloud.)
> >>>>
> >>>>
> >>>>
> >>>> I am (slowly) making progress on the research.
> >>>>
> >>>> I have the hardware and nearly have the proof
> >>>> checker from LEAN running on my FPGA.
> >>>>
> >>>> I'm in the process of spreading the DTPs from
> >>>> LEAN across the category/domain hierarchy.
> >>>>
> >>>> The current Axiom build extracts all of the functions
> >>>> but does not yet have the DTPs.
> >>>>
> >>>> I have to restructure the system, including the compiler
> >>>> and interpreter to parse and inherit the DTPs. I
> >>>> have some of that code but only some of the code
> >>>> has been pushed to the repository (volume 15) but
> >>>> that is rather trivial, out of date, and incomplete.
> >>>>
> >>>> I'm clearly not smart enough to prove the Risch
> >>>> algorithm and its associated machinery but the needed
> >>>> definitions and theorems will be available to someone
> >>>> who wants to try.
> >>>>
> >>>> [0] https://github.com/daly/PDFS/blob/master/bookvolbib.pdf
> >>>>
> >>>>
> >>>> On 8/19/21, Tim Daly <[email protected]> wrote:
> >>>>> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
> >>>>>
> >>>>> 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 /usr/bin/axiom to fix the bug:
> >>>>> (someone changed the axiom startup script.
> >>>>> It won't work on WSL2. I don't know who or
> >>>>> how to get it fixed).
> >>>>>
> >>>>> sudo emacs /usr/bin/axiom
> >>>>>
> >>>>> (split the line into 3 and add quote marks)
> >>>>>
> >>>>> export SPADDEFAULT=3D/usr/local/axiom/mnt/linux
> >>>>> export AXIOM=3D/usr/lib/axiom-20170501
> >>>>> export "PATH=3D/usr/lib/axiom-20170501/bin:$PATH"
> >>>>>
> >>>>> 4 WSL2) create a .axiom.input file to include startup cmds:
> >>>>>
> >>>>> emacs .axiom.input
> >>>>>
> >>>>> )cd "/mnt/c/yourpath"
> >>>>> )sys pwd
> >>>>>
> >>>>> 5 WSL2) create a "myaxiom" command that sets the
> >>>>>     DISPLAY variable and starts axiom
> >>>>>
> >>>>> emacs myaxiom
> >>>>>
> >>>>> #! /bin/bash
> >>>>> export DISPLAY=3D:0.0
> >>>>> axiom
> >>>>>
> >>>>> 6 WSL2) put it in the /usr/bin directory
> >>>>>
> >>>>> chmod +x myaxiom
> >>>>> sudo cp myaxiom /usr/bin/myaxiom
> >>>>>
> >>>>> 7 WINDOWS) start the X11 server
> >>>>>
> >>>>> (XMing XLaunch Icon on your desktop)
> >>>>>
> >>>>> 8 WINDOWS) run myaxiom from PowerShell
> >>>>> (this should start axiom with graphics available)
> >>>>>
> >>>>> wsl myaxiom
> >>>>>
> >>>>> 8 WINDOWS) make a PowerShell desktop
> >>>>>
> >>>>> https://superuser.com/questions/886951/run-powershell-script-when-yo=
u-open-powershell
> >>>>>
> >>>>> Tim
> >>>>>
> >>>>> On 8/13/21, Tim Daly <[email protected]> wrote:
> >>>>>> 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 interest is the ability to reason about
> >>>>>> and
> >>>>>> perform self-referential manipulations. In a dependently-typed
> >>>>>> system it seems interesting to be able "adapt" code to handle
> >>>>>> run-time computed arguments to dependent functions. The abstract:
> >>>>>>
> >>>>>>    "We show how a computational system can be constructed to
> >>>>>> "reason",
> >>>>>> effectively
> >>>>>>    and consequentially, about its own inferential processes. The
> >>>>>> analysis proceeds in two
> >>>>>>    parts. First, we consider the general question of computational
> >>>>>> semantics, rejecting
> >>>>>>    traditional approaches, and arguing that the declarative and
> >>>>>> procedural aspects of
> >>>>>>    computational symbols (what they stand for, and what behaviour
> >>>>>> they
> >>>>>> engender) should be
> >>>>>>    analysed independently, in order that they may be coherently
> >>>>>> related. Second, we
> >>>>>>    investigate self-referential behavior in computational processes=
,
> >>>>>> and show how to embed an
> >>>>>>    effective procedural model of a computational calculus within th=
at
> >>>>>> calculus (a model not
> >>>>>>    unlike a meta-circular interpreter, but connected to the
> >>>>>> fundamental operations of the
> >>>>>>    machine in such a way as to provide, at any point in a
> >>>>>> computation,
> >>>>>> fully articulated
> >>>>>>    descriptions of the state of that computation, for inspection an=
d
> >>>>>> possible modification). In
> >>>>>>    terms of the theories that result from these investigations, we
> >>>>>> present a general architecture
> >>>>>>    for procedurally reflective processes, able to shift smoothly
> >>>>>> between dealing with a given
> >>>>>>    subject domain, and dealing with their own reasoning processes
> >>>>>> over
> >>>>>> that domain.
> >>>>>>
> >>>>>>    An instance of the general solution is worked out in the context=

> >>>>>> of
> >>>>>> an applicative
> >>>>>>    language. Specifically, we present three successive dialects of
> >>>>>> LISP: 1-LISP, a distillation of
> >>>>>>    current practice, for comparison purposes; 2-LISP, a dialect
> >>>>>> constructed in terms of our
> >>>>>>    rationalised semantics, in which the concept of evaluation is
> >>>>>> rejected in favour of
> >>>>>>    independent notions of simplification and reference, and in whic=
h
> >>>>>> the respective categories
> >>>>>>    of notation, structure, semantics, and behaviour are strictly
> >>>>>> aligned; and 3-LISP, an
> >>>>>>    extension of 2-LISP endowed with reflective powers."
> >>>>>>
> >>>>>> Axiom SANE builds dependent types on the fly. The ability to access=

> >>>>>> both the refection
> >>>>>> of the tower of algebra and the reflection of the tower of proofs a=
t
> >>>>>> the time of construction
> >>>>>> makes the construction of a new domain or specific algorithm easier=

> >>>>>> and more general.
> >>>>>>
> >>>>>> This is of particular interest because one of the efforts is to bui=
ld
> >>>>>> "all the way down to the
> >>>>>> metal". If each layer is constructed on top of previous proven laye=
rs
> >>>>>> and the new layer
> >>>>>> can "reach below" to lower layers then the tower of layers can be
> >>>>>> built without duplication.
> >>>>>>
> >>>>>> Tim
> >>>>>>
> >>>>>> [0], Smith, Brian Cantwell "Reflection and Semantics in LISP"
> >>>>>> POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN
> >>>>>> ymposium on Principles of programming languagesJanuary 1
> >>>>>> 984 Pages 23=E2=80=9335https://doi.org/10.1145/800017.800513
> >>>>>>
> >>>>>> On 6/29/21, Tim Daly <[email protected]> wrote:
> >>>>>>> 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 algorithm parallel, such as a matrix multiply.
> >>>>>>>
> >>>>>>> But I think that it might be more effective to make each domain
> >>>>>>> run in parallel. A computation crosses multiple domains so a
> >>>>>>> particular computation could involve multiple parallel copies.
> >>>>>>>
> >>>>>>> For example, computing the Cylindrical Algebraic Decomposition
> >>>>>>> could recursively decompose the plane. Indeed, any tree-recursive
> >>>>>>> algorithm could be run in parallel "in the large" by creating new
> >>>>>>> running copies of the domain for each sub-problem.
> >>>>>>>
> >>>>>>> So the question becomes, how does one manage this?
> >>>>>>>
> >>>>>>> A similar problem occurs in robotics where one could have multiple=

> >>>>>>> wheels, arms, propellers, etc. that need to act independently but
> >>>>>>> in coordination.
> >>>>>>>
> >>>>>>> The robot solution uses ROS2. The three ideas are ROSCORE,
> >>>>>>> TOPICS with publish/subscribe, and SERVICES with request/response.=

> >>>>>>> These are communication paths defined between processes.
> >>>>>>>
> >>>>>>> ROS2 has a "roscore" which is basically a phonebook of "topics".
> >>>>>>> Any process can create or look up the current active topics. eq:
> >>>>>>>
> >>>>>>>    rosnode list
> >>>>>>>
> >>>>>>> TOPICS:
> >>>>>>>
> >>>>>>> Any process can PUBLISH a topic (which is basically a typed data
> >>>>>>> structure), e.g the topic /hw with the String data "Hello World".
> >>>>>>> eg:
> >>>>>>>
> >>>>>>>    rostopic pub /hw std_msgs/String "Hello, World"
> >>>>>>>
> >>>>>>> Any process can SUBSCRIBE to a topic, such as /hw, and get a
> >>>>>>> copy of the data.  eg:
> >>>>>>>
> >>>>>>>    rostopic echo /hw   =3D=3D> "Hello, World"
> >>>>>>>
> >>>>>>> Publishers talk, subscribers listen.
> >>>>>>>
> >>>>>>>
> >>>>>>> SERVICES:
> >>>>>>>
> >>>>>>> Any process can make a REQUEST of a SERVICE and get a RESPONSE.
> >>>>>>> This is basically a remote function call.
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>> Axiom in parallel?
> >>>>>>>
> >>>>>>> So domains could run, each in its own process. It could provide
> >>>>>>> services, one for each function. Any other process could request
> >>>>>>> a computation and get the result as a response. Domains could
> >>>>>>> request services from other domains, either waiting for responses
> >>>>>>> or continuing while the response is being computed.
> >>>>>>>
> >>>>>>> The output could be sent anywhere, to a terminal, to a browser,
> >>>>>>> to a network, or to another process using the publish/subscribe
> >>>>>>> protocol, potentially all at the same time since there can be many=

> >>>>>>> subscribers to a topic.
> >>>>>>>
> >>>>>>> Available domains could be dynamically added by announcing
> >>>>>>> themselves as new "topics" and could be dynamically looked-up
> >>>>>>> at runtime.
> >>>>>>>
> >>>>>>> This structure allows function-level / domain-level parallelism.
> >>>>>>> It is very effective in the robot world and I think it might be a
> >>>>>>> good structuring mechanism to allow computational mathematics
> >>>>>>> to take advantage of multiple processors in a disciplined fashion.=

> >>>>>>>
> >>>>>>> Axiom has a thousand domains and each could run on its own core.
> >>>>>>>
> >>>>>>> In addition. notice that each domain is independent of the others.=

> >>>>>>> So if we want to use BLAS Fortran code, it could just be another
> >>>>>>> service node. In fact, any "foreign function" could transparently
> >>>>>>> cooperate in a distributed Axiom.
> >>>>>>>
> >>>>>>> Another key feature is that proofs can be "by node".
> >>>>>>>
> >>>>>>> Tim
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>>
> >>>>>>> On 6/5/21, Tim Daly <[email protected]> wrote:
> >>>>>>>> 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 export a function to decide if a
> >>>>>>>> given type is "equivalent" to itself.
> >>>>>>>>
> >>>>>>>> The notion of "equivalence" might involve category ideas
> >>>>>>>> of natural transformation and univalence. Sigh.
> >>>>>>>>
> >>>>>>>> That's an interesting design point.
> >>>>>>>>
> >>>>>>>> Tim
> >>>>>>>>
> >>>>>>>>
> >>>>>>>> On 5/5/21, Tim Daly <[email protected]> wrote:
> >>>>>>>>> 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 o=
ne
> >>>>>>>>> of the many IDE tools I find they tend to "get in the way". I
> >>>>>>>>> already
> >>>>>>>>> know or can quickly find whatever they try to tell me. If you us=
e
> >>>>>>>>> an
> >>>>>>>>> IDE you probably find emacs "too sparse" for programming.
> >>>>>>>>>
> >>>>>>>>> Recently I've been working in a sparse programming environment.
> >>>>>>>>> I'm exploring the question of running a proof checker in an FPGA=
.
> >>>>>>>>> The FPGA development tools are painful at best and not intuitive=

> >>>>>>>>> since you SEEM to be programming but you're actually describing
> >>>>>>>>> hardware gates, connections, and timing. This is an environment
> >>>>>>>>> where everything happens all-at-once and all-the-time (like the
> >>>>>>>>> circuits in your computer). It is the "assembly language of
> >>>>>>>>> circuits".
> >>>>>>>>> Naturally, my eyes have adapted to this rather raw level.
> >>>>>>>>>
> >>>>>>>>> That said, I'm normally doing literate programming all the time.=

> >>>>>>>>> My typical file is a document which is a mixture of latex and
> >>>>>>>>> lisp.
> >>>>>>>>> It is something of a shock to return to that world. It is clear
> >>>>>>>>> why
> >>>>>>>>> people who program in Python find lisp to be a "sea of parens".
> >>>>>>>>> Yet as a lisp programmer, I don't even see the parens, just code=
.
> >>>>>>>>>
> >>>>>>>>> It takes a few minutes in a literate document to adapt vision to=

> >>>>>>>>> see the latex / lisp combination as natural. The latex markup,
> >>>>>>>>> like the lisp parens, eventually just disappears. What remains
> >>>>>>>>> is just lisp and natural language text.
> >>>>>>>>>
> >>>>>>>>> This seems painful at first but eyes quickly adapt. The upside
> >>>>>>>>> is that there is always a "finished" document that describes the=

> >>>>>>>>> state of the code. The overhead of writing a paragraph to
> >>>>>>>>> describe a new function or change a paragraph to describe the
> >>>>>>>>> changed function is very small.
> >>>>>>>>>
> >>>>>>>>> Using a Makefile I latex the document to generate a current PDF
> >>>>>>>>> and then I extract, load, and execute the code. This loop catche=
s
> >>>>>>>>> errors in both the latex and the source code. Keeping an open fi=
le
> >>>>>>>>> in
> >>>>>>>>> my pdf viewer shows all of the changes in the document after eve=
ry
> >>>>>>>>> run of make. That way I can edit the book as easily as the code.=

> >>>>>>>>>
> >>>>>>>>> Ultimately I find that writing the book while writing the code i=
s
> >>>>>>>>> more productive. I don't have to remember why I wrote something
> >>>>>>>>> since the explanation is already there.
> >>>>>>>>>
> >>>>>>>>> We all have our own way of programming and our own tools.
> >>>>>>>>> But I find literate programming to be a real advance over IDE
> >>>>>>>>> style programming and "raw code" programming.
> >>>>>>>>>
> >>>>>>>>> Tim
> >>>>>>>>>
> >>>>>>>>>
> >>>>>>>>> On 2/27/21, Tim Daly <[email protected]> wrote:
> >>>>>>>>>> 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 software architecture. See
> >>>>>>>>>> https://www.youtube.com/watch?v=3DW2hagw1VhhI&feature=3Dyoutu.b=
e
> >>>>>>>>>> and https://www.georgefairbanks.com/videos/
> >>>>>>>>>>
> >>>>>>>>>> My current thinking on SANE involves the ability to
> >>>>>>>>>> dynamically define categories, representations, and functions
> >>>>>>>>>> along with "composition functions" that permits choosing a
> >>>>>>>>>> combination at the time of use.
> >>>>>>>>>>
> >>>>>>>>>> You might want a domain for handling polynomials. There are
> >>>>>>>>>> a lot of choices, depending on your use case. You might want
> >>>>>>>>>> different representations. For example, you might want dense,
> >>>>>>>>>> sparse, recursive, or "machine compatible fixnums" (e.g. to
> >>>>>>>>>> interface with C code). If these don't exist it ought to be
> >>>>>>>>>> possible
> >>>>>>>>>> to create them. Such "lego-like" building blocks require carefu=
l
> >>>>>>>>>> thought about creating "fully factored" objects.
> >>>>>>>>>>
> >>>>>>>>>> Given that goal, the traditional barrier of "compiler" vs
> >>>>>>>>>> "interpreter"
> >>>>>>>>>> does not seem useful. It is better to "live within the compiler=
"
> >>>>>>>>>> which
> >>>>>>>>>> gives the ability to define new things "on the fly".
> >>>>>>>>>>
> >>>>>>>>>> Of course, the SANE compiler is going to want an associated
> >>>>>>>>>> proof of the functions you create along with the other parts
> >>>>>>>>>> such as its category hierarchy and representation properties.
> >>>>>>>>>>
> >>>>>>>>>> There is no such thing as a simple job. :-)
> >>>>>>>>>>
> >>>>>>>>>> Tim
> >>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>> On 2/18/21, Tim Daly <[email protected]> wrote:
> >>>>>>>>>>> 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 ty=
pe
> >>>>>>>>>>> construction at runtime. Both of these can occur in a runtime
> >>>>>>>>>>> object.
> >>>>>>>>>>> So there is potentially a mixture of interpreted and compiled
> >>>>>>>>>>> code.
> >>>>>>>>>>>
> >>>>>>>>>>> 2) It needs to perform type resolution at compile time without=

> >>>>>>>>>>> overhead
> >>>>>>>>>>> where possible. Since this is not always possible there needs t=
o
> >>>>>>>>>>> be
> >>>>>>>>>>> a "prefix thunk" that will perform the resolution. Trivially,
> >>>>>>>>>>> for
> >>>>>>>>>>> example,
> >>>>>>>>>>> if we have a + function we need to type-resolve the arguments.=

> >>>>>>>>>>>
> >>>>>>>>>>> However, if we can prove at compile time that the types are bo=
th
> >>>>>>>>>>> bounded-NNI and the result is bounded-NNI (i.e. fixnum in lisp=
)
> >>>>>>>>>>> then we can inline a call to + at runtime. If not, we might ha=
ve
> >>>>>>>>>>> + applied to NNI and POLY(FLOAT), which requires a thunk to
> >>>>>>>>>>> resolve types. The thunk could even "specialize and compile"
> >>>>>>>>>>> the code before executing it.
> >>>>>>>>>>>
> >>>>>>>>>>> It turns out that the Forth implementation of
> >>>>>>>>>>> "threaded-interpreted"
> >>>>>>>>>>> languages model provides an efficient and effective way to do
> >>>>>>>>>>> this.[0]
> >>>>>>>>>>> Type resolution can be "inserted" in intermediate thunks.
> >>>>>>>>>>> The model also supports dynamic overloading and tail recursion=
.
> >>>>>>>>>>>
> >>>>>>>>>>> Combining high-level CLOS code with low-level threading gives a=
n
> >>>>>>>>>>> easy to understand and robust design.
> >>>>>>>>>>>
> >>>>>>>>>>> Tim
> >>>>>>>>>>>
> >>>>>>>>>>> [0] Loeliger, R.G. "Threaded Interpretive Languages" (1981)
> >>>>>>>>>>> ISBN 0-07-038360-X
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>> On 2/5/21, Tim Daly <[email protected]> wrote:
> >>>>>>>>>>>> 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 source code, of course. But the=

> >>>>>>>>>>>> source
> >>>>>>>>>>>> code is not the only, nor possibly the best, representation o=
f
> >>>>>>>>>>>> the
> >>>>>>>>>>>> ideas.
> >>>>>>>>>>>> In particular, source code gets compiled into data structures=
.
> >>>>>>>>>>>> In
> >>>>>>>>>>>> Axiom
> >>>>>>>>>>>> these data structures really are a graph of related structure=
s.
> >>>>>>>>>>>>
> >>>>>>>>>>>> For example, looking at the gcd function from NNI, there is t=
he
> >>>>>>>>>>>> representation of the gcd function itself. But there is also a=

> >>>>>>>>>>>> structure
> >>>>>>>>>>>> that is the REP (and, in the new system, is separate from the=

> >>>>>>>>>>>> domain).
> >>>>>>>>>>>>
> >>>>>>>>>>>> Further, there are associated specification and proof
> >>>>>>>>>>>> structures.
> >>>>>>>>>>>> Even
> >>>>>>>>>>>> further, the domain inherits the category structures, and fro=
m
> >>>>>>>>>>>> those
> >>>>>>>>>>>> it
> >>>>>>>>>>>> inherits logical axioms and definitions through the proof
> >>>>>>>>>>>> structure.
> >>>>>>>>>>>>
> >>>>>>>>>>>> Clearly the gcd function is a node in a much larger graph
> >>>>>>>>>>>> structure.
> >>>>>>>>>>>>
> >>>>>>>>>>>> When trying to decide why code won't compile it would be usef=
ul
> >>>>>>>>>>>> to
> >>>>>>>>>>>> be able to see and walk these structures. I've thought about
> >>>>>>>>>>>> using
> >>>>>>>>>>>> the
> >>>>>>>>>>>> browser but browsers are too weak. Either everything has to b=
e
> >>>>>>>>>>>> "in
> >>>>>>>>>>>> a
> >>>>>>>>>>>> single tab to show the graph" or "the nodes of the graph are i=
n
> >>>>>>>>>>>> different
> >>>>>>>>>>>> tabs". Plus, constructing dynamic graphs that change as the
> >>>>>>>>>>>> software
> >>>>>>>>>>>> changes (e.g. by loading a new spad file or creating a new
> >>>>>>>>>>>> function)
> >>>>>>>>>>>> represents the huge problem of keeping the browser "in sync
> >>>>>>>>>>>> with
> >>>>>>>>>>>> the
> >>>>>>>>>>>> Axiom workspace". So something more dynamic and embedded is
> >>>>>>>>>>>> needed.
> >>>>>>>>>>>>
> >>>>>>>>>>>> Axiom source gets compiled into CLOS data structures. Each of=

> >>>>>>>>>>>> these
> >>>>>>>>>>>> new SANE structures has an associated surface representation,=

> >>>>>>>>>>>> so
> >>>>>>>>>>>> they
> >>>>>>>>>>>> can be presented in user-friendly form.
> >>>>>>>>>>>>
> >>>>>>>>>>>> Also, since Axiom is literate software, it should be possible=

> >>>>>>>>>>>> to
> >>>>>>>>>>>> look
> >>>>>>>>>>>> at
> >>>>>>>>>>>> the code in its literate form with the surrounding explanatio=
n.
> >>>>>>>>>>>>
> >>>>>>>>>>>> Essentially we'd like to have the ability to "deep dive" into=

> >>>>>>>>>>>> the
> >>>>>>>>>>>> Axiom
> >>>>>>>>>>>> workspace, not only for debugging, but also for understanding=

> >>>>>>>>>>>> what
> >>>>>>>>>>>> functions are used, where they come from, what they inherit,
> >>>>>>>>>>>> and
> >>>>>>>>>>>> how they are used in a computation.
> >>>>>>>>>>>>
> >>>>>>>>>>>> To that end I'm looking at using McClim, a lisp windowing
> >>>>>>>>>>>> system.
> >>>>>>>>>>>> Since the McClim windows would be part of the lisp image, the=
y
> >>>>>>>>>>>> have
> >>>>>>>>>>>> access to display (and modify) the Axiom workspace at all
> >>>>>>>>>>>> times.
> >>>>>>>>>>>>
> >>>>>>>>>>>> The only hesitation is that McClim uses quicklisp and drags i=
n
> >>>>>>>>>>>> a
> >>>>>>>>>>>> lot
> >>>>>>>>>>>> of other subsystems. It's all lisp, of course.
> >>>>>>>>>>>>
> >>>>>>>>>>>> These ideas aren't new. They were available on Symbolics
> >>>>>>>>>>>> machines,
> >>>>>>>>>>>> a truly productive platform and one I sorely miss.
> >>>>>>>>>>>>
> >>>>>>>>>>>> Tim
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>> On 1/19/21, Tim Daly <[email protected]> wrote:
> >>>>>>>>>>>>> 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 <[email protected]> wrote:
> >>>>>>>>>>>>>> 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 article is, to my mind, the most accurate account
> >>>>>>>>>>>>>> of what goes on in designing and coding a program.
> >>>>>>>>>>>>>> I refer to it regularly when discussing how much
> >>>>>>>>>>>>>> documentation to create, how to pass along tacit
> >>>>>>>>>>>>>> knowledge, and the value of the XP's metaphor-setting
> >>>>>>>>>>>>>> exercise. It also provides a way to examine a methodolgy's
> >>>>>>>>>>>>>> economic structure.
> >>>>>>>>>>>>>>
> >>>>>>>>>>>>>> In the article, which follows, note that the quality of the=

> >>>>>>>>>>>>>> designing programmer's work is related to the quality of
> >>>>>>>>>>>>>> the match between his theory of the problem and his theory
> >>>>>>>>>>>>>> of the solution. Note that the quality of a later
> >>>>>>>>>>>>>> programmer's
> >>>>>>>>>>>>>> work is related to the match between his theories and the
> >>>>>>>>>>>>>> previous programmer's theories.
> >>>>>>>>>>>>>>
> >>>>>>>>>>>>>> Using Naur's ideas, the designer's job is not to pass along=

> >>>>>>>>>>>>>> "the design" but to pass along "the theories" driving the
> >>>>>>>>>>>>>> design.
> >>>>>>>>>>>>>> The latter goal is more useful and more appropriate. It als=
o
> >>>>>>>>>>>>>> highlights that knowledge of the theory is tacit in the
> >>>>>>>>>>>>>> owning,
> >>>>>>>>>>>>>> and
> >>>>>>>>>>>>>> so passing along the thoery requires passing along both
> >>>>>>>>>>>>>> explicit
> >>>>>>>>>>>>>> and tacit knowledge.
> >>>>>>>>>>>>>>
> >>>>>>>>>>>>>> Tim
> >>>>>>>>>>>>>>
> >>>>>>>>>>>>>
> >>>>>>>>>>>>
> >>>>>>>>>>>
> >>>>>>>>>>
> >>>>>>>>>
> >>>>>>>>
> >>>>>>>
> >>>>>>
> >>>>>
> >>>>
> >>>
> >>
> >

--Apple-Mail-18CBE148-0FFC-47D9-9D95-5D7EFE73CB6B
Content-Transfer-Encoding: quoted-printable
Content-Type: text/html;
	charset=utf-8

<html><head></head><body bgcolor=3D"#FFFFFF"><div>The setup of a spreadsheet=
 is similar to the design of some prototype based programming languages. I h=
ave recently been learning about the Self programming language, a descendant=
 of Smalltalk, which uses prototypes rather than classes. This creates a mor=
e dynamic environment.</div><div><br></div><div>Like Smalltalk, development i=
s done using a virtual machine with a programming environment. The objects i=
n the Self environment can be configured using direct manipulation to define=
 behavior and inheritance.<br></div><div><br></div><a href=3D"https://selfla=
nguage.org/">https://selflanguage.org/</a><div><br></div><div>It should be p=
ossible to develop a similar prototype system based in lisp, if it has not b=
een done already.<br><div><br>On Mar 23, 2022, at 1:53, Tim Daly &lt;<a href=
=3D"mailto:[email protected]">[email protected]</a>&gt; wrote:<br><br></di=
v><div></div><blockquote type=3D"cite"><div><div dir=3D"ltr"><div>I have a d=
eep interest in self-modifying programs. These are</div><div>trivial to crea=
te in lisp. The question is how to structure a computer</div><div>algebra pr=
ogram so it could be dynamically modified but still <br></div><div>well-stru=
ctured. This is especially important since the user can</div><div>create new=
 logical types at runtime.</div><div><br></div><div>One innovation, which I h=
ave never seen anywhere, is to structure</div><div>the program in a spreadsh=
eet fashion. Spreadsheets cells can</div><div>reference other spreadsheet ce=
lls. Spreadsheets have a well-defined</div><div>evaluation method. This is e=
quivalent to a form of object-oriented</div><div>programming where each cell=
 is an object and has a well-defined</div><div>inheritance hierarchy through=
 other cells. Simple manipulation</div><div>allows insertion, deletion, or m=
odification of these chains at any time.</div><div><br></div><div>So by stru=
cturing a computer algebra program like a spreadsheet</div><div>I am able to=
 dynamically adjust a program to fit the problem to be</div><div>solved, tra=
ck which cells are needed, and optimize the program.</div><div><br></div><di=
v>Spreadsheets do this naturally but I'm unaware of any non-spreadsheet</div=
><div>program that relies on that organization.</div><div><br></div><div>Tim=
</div><div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" c=
lass=3D"gmail_attr">On Sun, Mar 13, 2022 at 4:01 AM Tim Daly &lt;<a href=3D"=
mailto:[email protected]">[email protected]</a>&gt; wrote:<br></div><block=
quote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1p=
x solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>Axiom has a=
n awkward 'attributes' category structure.</div><div><br></div><div>In the S=
ANE version it is clear that these attributes are much</div><div>closer to l=
ogic 'definitions'. As a result one of the changes</div><div>is to create a n=
ew 'category'-type structure for definitions.</div><div>There will be a new k=
eyword, like the category keyword,</div><div>'definition'.</div><div><br></d=
iv><div>Tim</div><div><br></div></div><br><div class=3D"gmail_quote"><div di=
r=3D"ltr" class=3D"gmail_attr">On Fri, Mar 11, 2022 at 9:46 AM Tim Daly &lt;=
<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]</=
a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px=
 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div=
 dir=3D"ltr"><div>The github lockout continues... <br></div><div><br></div><=
div>I'm spending some time adding examples to source code.</div><div><br></d=
iv><div>Any function can have ++X comments added. These will</div><div>appea=
r as examples when the function is )display For example,</div><div>in Permut=
ationGroup there is a function 'strongGenerators'</div><div>defined as:</div=
><div><br></div><div>&nbsp; strongGenerators : % -&gt; L PERM S</div><div>&n=
bsp;&nbsp;&nbsp; ++ strongGenerators(gp) returns strong generators for</div>=
<div>&nbsp;&nbsp;&nbsp; ++ the group gp.</div><div>&nbsp;&nbsp;&nbsp; ++</di=
v><div>&nbsp;&nbsp;&nbsp; ++X S:List(Integer) :=3D [1,2,3,4]</div><div>&nbsp=
;&nbsp;&nbsp; ++X G :=3D symmetricGroup(S)</div><div>&nbsp;&nbsp;&nbsp; ++X s=
trongGenerators(G)</div><div><br></div><div><br></div><div><br></div><div>La=
ter, in the interpreter we see:</div><div><br></div><div><br></div><div><br>=
</div><div><br></div><div>)d op strongGenerators</div><div><br></div><div>&n=
bsp; There is one exposed function called strongGenerators :</div><div>&nbsp=
;&nbsp;&nbsp;&nbsp;&nbsp; [1] PermutationGroup(D2) -&gt; List(Permutation(D2=
)) from</div><div>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbs=
p;&nbsp;&nbsp;&nbsp;&nbsp; PermutationGroup(D2)</div><div>&nbsp;&nbsp;&nbsp;=
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbs=
p; if D2 has SETCAT</div><div><br></div><div>&nbsp; Examples of strongGenera=
tors from PermutationGroup</div><div>&nbsp; <br></div><div>&nbsp; S:List(Int=
eger) :=3D [1,2,3,4]</div><div>&nbsp; G :=3D symmetricGroup(S)</div><div>&nb=
sp; strongGenerators(G)</div><div><br></div><div><br></div><div><br></div><d=
iv><br></div><div>This will show a working example for functions that the</d=
iv><div>user can copy and use. It is especially useful to show how</div><div=
>to construct working arguments.</div><div><br></div><div>These "example" fu=
nctions are run at build time when</div><div>the make command looks like</di=
v><div>&nbsp;&nbsp;&nbsp; make TESTSET=3Dalltests<br></div><div><br></div><d=
iv>I hope to add this documentation to all Axiom functions.</div><div><br></=
div><div>In addition, the plan is to add these function calls to the</div><d=
iv>usual test documentation. That means that all of these examples</div><div=
>will be run and show their output in the final distribution</div><div>(mnt/=
ubuntu/doc/src/input/*.dvi files) so the user can view</div><div>the expecte=
d output.<br></div><div><br></div><div>Tim</div><div><br></div><div><br></di=
v><div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=
=3D"gmail_attr">On Fri, Feb 25, 2022 at 6:05 PM Tim Daly &lt;<a href=3D"mail=
to:[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<b=
r></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;=
border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><d=
iv>It turns out that creating SPAD-looking output is trivial <br></div><div>=
in Common Lisp. Each class can have a custom print</div><div>routine so sign=
atures and ++ comments can each be</div><div>printed with their own format.<=
/div><div><br></div><div>To ensure that I maintain compatibility I'll be pri=
nting</div><div>the categories and domains so they look like SPAD code,</div=
><div>at least until I get the proof technology integrated. I will</div><div=
>probably specialize the proof printers to look like the</div><div>original L=
EAN proof syntax.</div><div><br></div><div>Internally, however, it will all b=
e Common Lisp.</div><div><br></div><div>Common Lisp makes so many desirable f=
eatures so easy.</div><div>It is possible to trace dynamically at any level.=
 One could</div><div>even write a trace that showed how Axiom arrived at the=
</div><div>solution. Any domain could have special case output syntax</div><=
div>without affecting any other domain so one could write a</div><div>tree-l=
ike output for proofs. Using greek characters is trivial</div><div>so the in=
put and output notation is more mathematical.<br></div><div><br></div><div>T=
im</div><div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr"=
 class=3D"gmail_attr">On Thu, Feb 24, 2022 at 10:24 AM Tim Daly &lt;<a href=3D=
"mailto:[email protected]" target=3D"_blank">[email protected]</a>&gt; wro=
te:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0=
.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"lt=
r"><div>Axiom's SPAD code compiles to Common Lisp.</div><div>The AKCL versio=
n of Common Lisp compiles to C.</div><div>Three languages and 2 compilers is=
 a lot to maintain.</div><div>Further, there are very few people able to wri=
te SPAD</div><div>and even fewer people able to maintain it.<br></div><div><=
br></div><div>I've decided that the SANE version of Axiom will be <br></div>=
<div>implemented in pure Common Lisp. I've outlined Axiom's<br></div><div>ca=
tegory / type hierarchy in the Common Lisp Object</div><div>System (CLOS). I=
 am now experimenting with re-writing</div><div>the functions into Common Li=
sp.<br></div><div><br></div><div>This will have several long-term effects. I=
t simplifies</div><div>the implementation issues. SPAD code blocks a lot of<=
/div><div>actions and optimizations that Common Lisp provides.</div><div>The=
 Common Lisp language has many more people<br></div><div>who can read, modif=
y, and maintain code. It provides for</div><div>interoperability with other C=
ommon Lisp projects with</div><div>no effort. Common Lisp is an internationa=
l standard</div><div>which ensures that the code will continue to run.<br></=
div><div><br></div><div>The input / output mathematics will remain the same.=
</div><div>Indeed, with the new generalizations for first-class</div><div>de=
pendent types it will be more general.</div><div><br></div><div>This is a bi=
g change, similar to eliminating BOOT code</div><div>and moving to Literate P=
rogramming. This will provide a</div><div>better platform for future researc=
h work. Current research</div><div>is focused on merging Axiom's computer al=
gebra mathematics</div><div>with Lean's proof language. The goal is to creat=
e a system for</div><div>&nbsp;"computational mathematics".<br></div><div><b=
r></div><div>Research is the whole point of Axiom.</div><div><br></div><div>=
Tim</div><div><br></div><div><br></div></div><br><div class=3D"gmail_quote">=
<div dir=3D"ltr" class=3D"gmail_attr">On Sat, Jan 22, 2022 at 9:16 PM Tim Da=
ly &lt;<a href=3D"mailto:[email protected]" target=3D"_blank">axiomcas@gmai=
l.com</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"mar=
gin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1e=
x"><div dir=3D"ltr"><div>I can't stress enough how important it is to listen=
 to Hamming's talk</div><div><a href=3D"https://www.youtube.com/watch?v=3Da1=
zDuOPkMSw" target=3D"_blank">https://www.youtube.com/watch?v=3Da1zDuOPkMSw</=
a></div><div><br></div><div>Axiom will begin to die the day I stop working o=
n it.</div><div><br></div><div>However, proving Axiom correct "down to the m=
etal", is fundamental.</div><div>It will merge computer algebra and logic, s=
pawning years of new</div><div>research.</div><div><br></div><div>Work on fu=
ndamental problems.</div><div><br></div><div>Tim</div><div><br></div></div><=
br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, D=
ec 30, 2021 at 6:46 PM Tim Daly &lt;<a href=3D"mailto:[email protected]" ta=
rget=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote class=
=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb=
(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>One of the interesting=
 questions when obtaining a result</div><div>is "what functions were called a=
nd what was their return value?"</div><div>Otherwise known as the "show your=
 work" idea.</div><div><br></div><div>There is an idea called the "writer mo=
nad" [0], usually <br></div><div>implemented to facilitate logging. We can e=
xploit this</div><div>idea to provide "show your work" capability. Each func=
tion</div><div>can provide this information inside the monad enabling the</d=
iv><div>question to be answered at any time.</div><div><br></div><div>For th=
ose unfamiliar with the monad idea, the best explanation</div><div>I've foun=
d is this video [1].</div><div><br></div><div>Tim<br></div><div><br></div><d=
iv>[0] Deriving the writer monad from first principles<br></div><div><a href=
=3D"https://williamyaoh.com/posts/2020-07-26-deriving-writer-monad.html" tar=
get=3D"_blank">https://williamyaoh.com/posts/2020-07-26-deriving-writer-mona=
d.html</a></div><div><br></div><div>[1] The Absolute Best Intro to Monads fo=
r Software Engineers</div><div><a href=3D"https://www.youtube.com/watch?v=3D=
C2w45qRc3aU" target=3D"_blank">https://www.youtube.com/watch?v=3DC2w45qRc3aU=
</a></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gma=
il_attr">On Mon, Dec 13, 2021 at 12:30 AM Tim Daly &lt;<a href=3D"mailto:axi=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br></di=
v><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border=
-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>...=
(snip)...<br></div><div><br></div><div>Common Lisp has an "open compiler". T=
hat allows the ability</div><div>to deeply modify compiler behavior using co=
mpiler macros</div><div>and macros in general. CLOS takes advantage of this t=
o add</div><div>typed behavior into the compiler in a way that ALLOWS strict=
</div><div>typing such as found in constructive type theory and ML.</div><di=
v>Judgments, ala Crary, are front-and-center.<br></div><div><br></div><div>W=
hether you USE the discipline afforded is the real question.</div><div><br><=
/div><div>Indeed, the Axiom research struggle is essentially one of how</div=
><div>to have a disciplined use of first-class dependent types. The</div><di=
v>struggle raises issues of, for example, compiling a dependent</div><div>ty=
pe whose argument is recursive in the compiled type. Since</div><div>the new=
 type is first-class it can be constructed at what you</div><div>improperly c=
all "run-time". However, it appears that the recursive</div><div>type may ha=
ve to call the compiler at each recursion to generate</div><div>the next ste=
p since in some cases it cannot generate "closed code".<br></div><div><br></=
div><div>I am embedding proofs (in LEAN language) into the type</div><div>hi=
erarchy so that theorems, which depend on the type hierarchy,<br></div><div>=
are correctly inherited. The compiler has to check the proofs of functions</=
div><div>at compile time using these. Hacking up nonsense just won't cut it.=
 Think</div><div>of the problem of embedding LEAN proofs in ML or ML in LEAN=
.</div><div>(Actually, Jeremy Avigad might find that research interesting.)<=
/div><div><br></div><div>So Matrix(3,3,Float) has inverses (assuming Float i=
s a</div><div>field (cough)). The type inherits this theorem and proofs of</=
div><div>functions can use this. But Matrix(3,4,Integer) does not have</div>=
<div>inverses so the proofs cannot use this. The type hierarchy has</div><di=
v>to ensure that the proper theorems get inherited.<br></div><div><br></div>=
<div>Making proof technology work at compile time is hard.</div><div>(Worse y=
et, LEAN is a moving target. Sigh.)<br></div><div><br><br></div></div><br><d=
iv class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu, Nov 2=
5, 2021 at 9:43 AM Tim Daly &lt;<a href=3D"mailto:[email protected]" target=
=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"=
gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204=
,204,204);padding-left:1ex"><div dir=3D"ltr"><div dir=3D"ltr"><div><br></div=
><div dir=3D"ltr"><div>As you know I've been re-architecting Axiom to use fi=
rst class</div><div>dependent types and proving the algorithms correct. For e=
xample,</div><div>the GCD of natural numbers or the GCD of polynomials.</div=
><div><br></div><div>The idea involves "boxing up" the proof with the algori=
thm (aka</div><div>proof carrying code) in the ELF file (under a crypto hash=
 so it</div><div>can't be changed).</div><div><br></div><div>Once the code i=
s running on the CPU, the proof is run in parallel</div><div>on the field pr=
ogrammable gate array (FPGA). Intel data center</div><div>servers have CPUs w=
ith built-in FPGAs these days.</div><div><br></div><div>There is a bit of a d=
isconnect, though. The GCD code is compiled</div><div>machine code but the p=
roof is LEAN-level.</div><div><br></div><div>What would be ideal is if the c=
ompiler not only compiled the GCD</div><div>code to machine code, it also co=
mpiled the proof to "machine code".</div><div>That is, for each machine inst=
ruction, the FPGA proof checker</div><div>would ensure that the proof was no=
t violated at the individual</div><div>instruction level.<br></div><div><br>=
</div><div>What does it mean to "compile a proof to the machine code level"?=
</div><div><br></div><div>The Milawa effort (Myre14.pdf) does incremental pr=
oofs in layers.</div><div>To quote from the article [0]:<br></div><div><br><=
/div><div>&nbsp;&nbsp; We begin with a simple proof checker, call it A, whic=
h is short</div><div>&nbsp;&nbsp; enough to verify by the ``social process''=
 of mathematics -- and</div><div>&nbsp; more recently with a theorem prover f=
or a more expressive logic.</div><div><br></div><div>&nbsp;&nbsp; We then de=
velop a series of increasingly powerful proof checkers,</div><div>&nbsp; cal=
l the B, C, D, and so on. We show each of these programs only</div><div>&nbs=
p;&nbsp; accepts the same formulas as A, using A to verify B, and B to verif=
y</div><div>&nbsp;&nbsp; C, and so on. Then, since we trust A, and A says B i=
s trustworthy, we</div><div>&nbsp;&nbsp; can trust B. Then, since we trust B=
, and B says C is trustworthy, we</div><div>&nbsp;&nbsp; can trust C. <br></=
div><div><br></div><div>This gives a technique for "compiling the proof" dow=
n the the machine</div><div>code level. Ideally, the compiler would have jud=
gments for each step of</div><div>the compilation so that each compile step h=
as a justification. I don't</div><div>know of any compiler that does this ye=
t. (References welcome).<br></div><div><div><br></div><div>At the machine co=
de level, there are techniques that would allow</div><div>the FPGA proof to "=
step in sequence" with the executing code.<br></div><div>Some work has been d=
one on using "Hoare Logic for Realistically</div><div>Modelled Machine Code"=
 (paper attached, Myre07a.pdf),</div><div>"Decompilation into Logic -- Impro=
ved (Myre12a.pdf).</div><div><br></div><div>So the game is to construct a GC=
D over some type (Nats, Polys, etc.</div><div>Axiom has 22), compile the dep=
endent type GCD to machine code.</div><div>In parallel, the proof of the cod=
e is compiled to machine code. The</div><div>pair is sent to the CPU/FPGA an=
d, while the algorithm runs, the FPGA</div><div>ensures the proof is not vio=
lated, instruction by instruction.</div><div><br></div><div>(I'm ignoring ma=
chine architecture issues such pipelining, out-of-order,</div><div>branch pr=
ediction, and other machine-level things to ponder. I'm looking</div><div>at=
 the RISC-V Verilog details by various people to understand better but</div>=
<div>it is still a "misty fog" for me.)<br></div><div><br></div><div>The res=
ult is proven code "down to the metal".</div><div><br></div><div>Tim</div><d=
iv><br></div><div><br></div><div><br></div><div>[0] <a href=3D"https://www.c=
s.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____M=
ILAWA" target=3D"_blank">https://www.cs.utexas.edu/users/moore/acl2/manuals/=
current/manual/index-seo.php/ACL2____MILAWA</a></div></div></div></div></div=
><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Thu=
, Nov 25, 2021 at 6:05 AM Tim Daly &lt;<a href=3D"mailto:[email protected]"=
 target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote cl=
ass=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid r=
gb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><br><div dir=3D"ltr"><div=
>As you know I've been re-architecting Axiom to use first class</div><div>de=
pendent types and proving the algorithms correct. For example,</div><div>the=
 GCD of natural numbers or the GCD of polynomials.</div><div><br></div><div>=
The idea involves "boxing up" the proof with the algorithm (aka</div><div>pr=
oof carrying code) in the ELF file (under a crypto hash so it</div><div>can'=
t be changed).</div><div><br></div><div>Once the code is running on the CPU,=
 the proof is run in parallel</div><div>on the field programmable gate array=
 (FPGA). Intel data center</div><div>servers have CPUs with built-in FPGAs t=
hese days.</div><div><br></div><div>There is a bit of a disconnect, though. T=
he GCD code is compiled</div><div>machine code but the proof is LEAN-level.<=
/div><div><br></div><div>What would be ideal is if the compiler not only com=
piled the GCD</div><div>code to machine code, it also compiled the proof to "=
machine code".</div><div>That is, for each machine instruction, the FPGA pro=
of checker</div><div>would ensure that the proof was not violated at the ind=
ividual</div><div>instruction level.<br></div><div><br></div><div>What does i=
t mean to "compile a proof to the machine code level"?</div><div><br></div><=
div>The Milawa effort (Myre14.pdf) does incremental proofs in layers.</div><=
div>To quote from the article [0]:<br></div><div><br></div><div>&nbsp;&nbsp;=
 We begin with a simple proof checker, call it A, which is short</div><div>&=
nbsp;&nbsp; enough to verify by the ``social process'' of mathematics -- and=
</div><div>&nbsp; more recently with a theorem prover for a more expressive l=
ogic.</div><div><br></div><div>&nbsp;&nbsp; We then develop a series of incr=
easingly powerful proof checkers,</div><div>&nbsp; call the B, C, D, and so o=
n. We show each of these programs only</div><div>&nbsp;&nbsp; accepts the sa=
me formulas as A, using A to verify B, and B to verify</div><div>&nbsp;&nbsp=
; C, and so on. Then, since we trust A, and A says B is trustworthy, we</div=
><div>&nbsp;&nbsp; can trust B. Then, since we trust B, and B says C is trus=
tworthy, we</div><div>&nbsp;&nbsp; can trust C. <br></div><div><br></div><di=
v>This gives a technique for "compiling the proof" down the the machine</div=
><div>code level. Ideally, the compiler would have judgments for each step o=
f</div><div>the compilation so that each compile step has a justification. I=
 don't</div><div>know of any compiler that does this yet. (References welcom=
e).<br></div><div><div><br></div><div>At the machine code level, there are t=
echniques that would allow</div><div>the FPGA proof to "step in sequence" wi=
th the executing code.<br></div><div>Some work has been done on using "Hoare=
 Logic for Realistically</div><div>Modelled Machine Code" (paper attached, M=
yre07a.pdf),</div><div>"Decompilation into Logic -- Improved (Myre12a.pdf).<=
/div><div><br></div><div>So the game is to construct a GCD over some type (N=
ats, Polys, etc.</div><div>Axiom has 22), compile the dependent type GCD to m=
achine code.</div><div>In parallel, the proof of the code is compiled to mac=
hine code. The</div><div>pair is sent to the CPU/FPGA and, while the algorit=
hm runs, the FPGA</div><div>ensures the proof is not violated, instruction b=
y instruction.</div><div><br></div><div>(I'm ignoring machine architecture i=
ssues such pipelining, out-of-order,</div><div>branch prediction, and other m=
achine-level things to ponder. I'm looking</div><div>at the RISC-V Verilog d=
etails by various people to understand better but</div><div>it is still a "m=
isty fog" for me.)<br></div><div><br></div><div>The result is proven code "d=
own to the metal".</div><div><br></div><div>Tim</div><div><br></div><div><br=
></div><div><br></div><div>[0] <a href=3D"https://www.cs.utexas.edu/users/mo=
ore/acl2/manuals/current/manual/index-seo.php/ACL2____MILAWA" target=3D"_bla=
nk">https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-=
seo.php/ACL2____MILAWA</a></div></div></div></div><br><div class=3D"gmail_qu=
ote"><div dir=3D"ltr" class=3D"gmail_attr">On Sat, Nov 13, 2021 at 5:28 PM T=
im Daly &lt;<a href=3D"mailto:[email protected]" target=3D"_blank">axiomcas=
@gmail.com</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D=
"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-lef=
t:1ex"><div dir=3D"ltr"><div>Full support for general, first-class dependent=
 types requires</div><div>some changes to the Axiom design. That implies som=
e language</div><div>design questions.</div><div><br></div><div>Given that m=
athematics is such a general subject with a lot of</div><div>"local" notatio=
n and ideas (witness logical judgment notation)</div><div>careful thought is=
 needed to design a language that is able to</div><div>handle a wide range.<=
/div><div><br></div><div>Normally language design is a two-level process. Th=
e language</div><div>designer creates a language and then an implementation.=
 Various</div><div>design choices affect the final language.<br></div><div><=
br></div><div>There is "The Metaobject Protocol" (MOP)<br></div><div><a href=
=3D"https://www.amazon.com/Art-Metaobject-Protocol-Gregor-Kiczales/dp/026261=
0744" target=3D"_blank">https://www.amazon.com/Art-Metaobject-Protocol-Grego=
r-Kiczales/dp/0262610744</a></div><div>which encourages a three-level proces=
s. The language designer <br></div><div>works at a Metalevel to design a fam=
ily of languages, then the</div><div>language specializations, then the impl=
ementation. A MOP design</div><div>allows the language user to optimize the l=
anguage to their problem.</div><div><br></div><div>A simple paper on the sub=
ject is "Metaobject Protocols"</div><div><a href=3D"https://users.cs.duke.ed=
u/~vahdat/ps/mop.pdf" target=3D"_blank">https://users.cs.duke.edu/~vahdat/ps=
/mop.pdf</a></div><div><br></div><div>Tim</div><div><br></div></div><br><div=
 class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Mon, Oct 25,=
 2021 at 7:42 PM Tim Daly &lt;<a href=3D"mailto:[email protected]" target=3D=
"_blank">[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"gma=
il_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,20=
4,204);padding-left:1ex"><div dir=3D"ltr"><div>I have a separate thread of r=
esearch on Self-Replicating Systems</div><div>(ref: Kinematics of Self Repro=
ducing Machines</div><div><a href=3D"http://www.molecularassembler.com/KSRM.=
htm" target=3D"_blank">http://www.molecularassembler.com/KSRM.htm</a>)<br></=
div><div><br></div><div>which led to watching "Strange Dreams of Stranger Lo=
ops" by Will Byrd</div><div><a href=3D"https://www.youtube.com/watch?v=3DAff=
W-7ika0E" target=3D"_blank">https://www.youtube.com/watch?v=3DAffW-7ika0E</a=
></div><div><br></div><div>Will referenced a PhD Thesis by Jon Doyle</div><d=
iv>"A Model for Deliberation, Action, and Introspection"</div><div><br></div=
><div>I also read the thesis by J.C.G. Sturdy</div><div>"A Lisp through the L=
ooking Glass"</div><div><br></div><div>Self-replication requires the ability=
 to manipulate your own</div><div>representation in such a way that changes t=
o that representation</div><div>will change behavior.</div><div><br></div><d=
iv>This leads to two thoughts in the SANE research.</div><div><br></div><div=
>First, "Declarative Representation". That is, most of the things</div><div>=
about the representation should be declarative rather than</div><div>procedu=
ral. Applying this idea as much as possible makes it</div><div>easier to und=
erstand and manipulate.<br></div><div><br></div><div>Second, "Explicit Call S=
tack". Function calls form an implicit</div><div>call stack. This can usuall=
y be displayed in a running lisp system.</div><div>However, having the call s=
tack explicitly available would mean</div><div>that a system could "introspe=
ct" at the first-class level.</div><div><br></div><div>These two ideas would=
 make it easy, for example, to let the</div><div>system "show the work". One=
 of the normal complaints is that</div><div>a system presents an answer but t=
here is no way to know how</div><div>that answer was derived. These two idea=
s make it possible to</div><div>understand, display, and even post-answer ma=
nipulate</div><div>the intermediate steps.</div><div><br></div><div>Having t=
he intermediate steps also allows proofs to be</div><div>inserted in a step-=
by-step fashion. This aids the effort to</div><div>have proofs run in parall=
el with computation at the hardware</div><div>level.<br></div><div><br></div=
><div>Tim</div><div><br></div><div><br></div><div><br></div><div><br></div><=
div><br> </div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D=
"gmail_attr">On Thu, Oct 21, 2021 at 9:50 AM Tim Daly &lt;<a href=3D"mailto:=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br><=
/div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;bor=
der-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>=
So the current struggle involves the categories in Axiom.</div><div><br></di=
v><div>The categories and domains constructed using categories</div><div>are=
 dependent types. When are dependent types "equal"?</div><div>Well, hummmm, t=
hat depends on the arguments to the</div><div>constructor.</div><div><br></d=
iv><div>But in order to decide(?) equality we have to evaluate</div><div>the=
 arguments (which themselves can be dependent types).</div><div>Indeed, we m=
ay, and in general, we must evaluate the <br></div><div>arguments at compile=
 time (well, "construction time" as</div><div>there isn't really a compiler /=
 interpreter separation anymore.)<br></div><div><br></div><div>That raises t=
he question of what "equality" means. This</div><div>is not simply a "set eq=
uality" relation. It falls into the</div><div>infinite-groupoid of homotopy t=
ype theory. In general</div><div>it appears that deciding category / domain e=
quivalence</div><div>might force us to climb the type hierarchy.</div><div><=
br></div><div>Beyond that, there is the question of "which proof"</div><div>=
applies to the resulting object. Proofs depend on their</div><div>assumption=
s which might be different for different</div><div>constructions. As yet I h=
ave no clue how to "index"</div><div>proofs based on their assumptions, nor h=
ow to <br></div><div>connect these assumptions to the groupoid structure.</d=
iv><div><br></div><div>My brain hurts.</div><div><br></div><div>Tim</div><di=
v><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"g=
mail_attr">On Mon, Oct 18, 2021 at 2:00 AM Tim Daly &lt;<a href=3D"mailto:ax=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br></d=
iv><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;borde=
r-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><div>"B=
irthing Computational Mathematics"</div><div><br></div><div>The Axiom SANE p=
roject is difficult at a very fundamental</div><div>level. The title "SANE" w=
as chosen due to the various</div><div>words found in a thesuarus... "ration=
al", "coherent",</div><div>"judicious" and "sound".</div><div><br></div><div=
>These are very high level, amorphous ideas. But so is</div><div>the design o=
f SANE. Breaking away from tradition in</div><div>computer algebra, type the=
ory, and proof assistants</div><div>is very difficult. Ideas tend to fall in=
to standard jargon</div><div>which limits both the frame of thinking (e.g. d=
ependent</div><div>types) and the content (e.g. notation).</div><div><br></d=
iv><div>Questioning both frame and content is very difficult.</div><div>It i=
s hard to even recognize when they are accepted</div><div>"by default" rathe=
r than "by choice". What does the idea<br></div><div>"power tools" mean in a=
 primitive, hand labor culture?<br></div><div><br></div><div>Christopher Ale=
xander [0] addresses this problem in</div><div>a lot of his writing. Specifi=
cally, in his book "Notes on</div><div>the Synthesis of Form", in his chapte=
r 5 "The Selfconsious</div><div>Process", he addresses this problem directly=
. This is a</div><div>"must read" book.<br></div><div><br></div><div>Unlike b=
uilding design and contruction, however, there</div><div>are almost no const=
raints to use as guides. Alexander</div><div>quotes Plato's Phaedrus:</div><=
div><br></div><div>&nbsp; "First, the taking in of scattered particulars und=
er</div><div>&nbsp;&nbsp; one Idea, so that everyone understands what is bei=
ng</div><div>&nbsp;&nbsp; talked about ... Second, the separation of the Ide=
a</div><div>&nbsp;&nbsp; into parts, by dividing it at the joints, as nature=
</div><div>&nbsp;&nbsp; directs, not breaking any limb in half as a bad <br>=
</div><div>&nbsp;&nbsp; carver might."<br></div><div><br></div><div>Lisp, wh=
ich has been called "clay for the mind" can</div><div>build virtually anythi=
ng that can be thought. The <br></div><div>"joints" are also "of one's choos=
ing" so one is</div><div>both carver and "nature".<br></div><div><br></div><=
div>Clearly the problem is no longer "the tools".</div><div>*I* am the probl=
em constraining the solution.</div><div>Birthing this "new thing" is slow, d=
ifficult, and</div><div>uncertain at best.</div><div><br></div><div>Tim</div=
><div><br></div><div>[0] Alexander, Christopher "Notes on the Synthesis</div=
><div>of Form" Harvard University Press 1964 <br></div><div>ISBN 0-674-62751=
-2</div><div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr"=
 class=3D"gmail_attr">On Sun, Oct 10, 2021 at 4:40 PM Tim Daly &lt;<a href=3D=
"mailto:[email protected]" target=3D"_blank">[email protected]</a>&gt; wro=
te:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0=
.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Re: writing a p=
aper... I'm not connected to Academia<br>
so anything I'd write would never make it into print.<br>
<br>
"Language level parsing" is still a long way off. The talk<br>
by Guy Steele [2] highlights some of the problems we<br>
currently face using mathematical metanotation.<br>
<br>
For example, a professor I know at CCNY (City College<br>
of New York) didn't understand Platzer's "funny<br>
fraction notation" (proof judgements) despite being<br>
an expert in Platzer's differential equations area.<br>
<br>
Notation matters and is not widely common.<br>
<br>
I spoke to Professor Black (in LTI) about using natural<br>
language in the limited task of a human-robot cooperation<br>
in changing a car tire.&nbsp; I looked at the current machine<br>
learning efforts. They are no where near anything but<br>
toy systems, taking too long to train and are too fragile.<br>
<br>
Instead I ended up using a combination of AIML [3]<br>
(Artificial Intelligence Markup Language), the ALICE<br>
Chatbot [4], Forgy's OPS5 rule based program [5],<br>
and Fahlman's SCONE [6] knowledge base. It was<br>
much less fragile in my limited domain problem.<br>
<br>
I have no idea how to extend any system to deal with<br>
even undergraduate mathematics parsing.<br>
<br>
Nor do I have any idea how I would embed LEAN<br>
knowledge into a SCONE database, although I<br>
think the combination would be useful and interesting.<br>
<br>
I do believe that, in the limited area of computational<br>
mathematics, we are capable of building robust, proven<br>
systems that are quite general and extensible. As you<br>
might have guessed I've given it a lot of thought over<br>
the years :-)<br>
<br>
A mathematical language seems to need &gt;6 components<br>
<br>
1) We need some sort of a specification language, possibly<br>
somewhat 'propositional' that introduces the assumptions<br>
you mentioned (ref. your discussion of numbers being<br>
abstract and ref. your discussion of relevant choice of<br>
assumptions related to a problem).<br>
<br>
This is starting to show up in the hardware area (e.g.<br>
Lamport's TLC[0])<br>
<br>
Of course, specifications relate to proving programs<br>
and, as you recall, I got a cold reception from the<br>
LEAN community about using LEAN for program proofs.<br>
<br>
2) We need "scaffolding". That is, we need a theory<br>
that can be reduced to some implementable form<br>
that provides concept-level structure.<br>
<br>
Axiom uses group theory for this. Axiom's "category"<br>
structure has "Category" things like Ring. Claiming<br>
to be a Ring brings in a lot of "Signatures" of functions<br>
you have to implement to properly be a Ring.<br>
<br>
Scaffolding provides a firm mathematical basis for<br>
design. It provides a link between the concept of a<br>
Ring and the expectations you can assume when<br>
you claim your "Domain" "is a Ring". Category<br>
theory might provide similar structural scaffolding<br>
(eventually... I'm still working on that thought garden)<br>
<br>
LEAN ought to have a textbook(s?) that structures<br>
the world around some form of mathematics. It isn't<br>
sufficient to say "undergraduate math" is the goal.<br>
There needs to be some coherent organization so<br>
people can bring ideas like Group Theory to the<br>
organization. Which brings me to ...<br>
<br>
3) We need "spreading". That is, we need to take<br>
the various definitions and theorems in LEAN and<br>
place them in their proper place in the scaffold.<br>
<br>
For example, the Ring category needs the definitions<br>
and theorems for a Ring included in the code for the<br>
Ring category. Similarly, the Commutative category<br>
needs the definitions and theorems that underlie<br>
"commutative" included in the code.<br>
<br>
That way, when you claim to be a "Commutative Ring"<br>
you get both sets of definitions and theorems. That is,<br>
the inheritance mechanism will collect up all of the<br>
definitions and theorems and make them available<br>
for proofs.<br>
<br>
I am looking at LEAN's definitions and theorems with<br>
an eye to "spreading" them into the group scaffold of<br>
Axiom.<br>
<br>
4) We need "carriers" (Axiom calls them representations,<br>
aka "REP"). REPs allow data structures to be defined<br>
independent of the implementation.<br>
<br>
For example, Axiom can construct Polynomials that<br>
have their coefficients in various forms of representation.<br>
You can define "dense" (all coefficients in a list),<br>
"sparse" (only non-zero coefficients), "recursive", etc.<br>
<br>
A "dense polynomial" and a "sparse polynomial" work<br>
exactly the same way as far as the user is concerned.<br>
They both implement the same set of functions. There<br>
is only a difference of representation for efficiency and<br>
this only affects the implementation of the functions,<br>
not their use.<br>
<br>
Axiom "got this wrong" because it didn't sufficiently<br>
separate the REP from the "Domain". I plan to fix this.<br>
<br>
LEAN ought to have a "data structures" subtree that<br>
has all of the definitions and axioms for all of the<br>
existing data structures (e.g. Red-Black trees). This<br>
would be a good undergraduate project.<br>
<br>
5) We need "Domains" (in Axiom speak). That is, we<br>
need a box that holds all of the functions that implement<br>
a "Domain". For example, a "Polynomial Domain" would<br>
hold all of the functions for manipulating polynomials<br>
(e.g polynomial multiplication). The "Domain" box<br>
is a dependent type that:<br>
<br>
&nbsp; A) has an argument list of "Categories" that this "Domain"<br>
&nbsp; &nbsp; &nbsp; box inherits. Thus, the "Integer Domain" inherits<br>
&nbsp; &nbsp; &nbsp; the definitions and axioms from "Commutative"<br>
<br>
&nbsp; &nbsp; &nbsp;Functions in the "Domain" box can now assume<br>
&nbsp; &nbsp; &nbsp;and use the properties of being commutative. Proofs<br>
&nbsp; &nbsp; &nbsp;of functions in this domain can use the definitions<br>
&nbsp; &nbsp; &nbsp;and proofs about being commutative.<br>
<br>
&nbsp; B) contains an argument that specifies the "REP"<br>
&nbsp; &nbsp; &nbsp; &nbsp;(aka, the carrier). That way you get all of the<b=
r>
&nbsp; &nbsp; &nbsp; &nbsp;functions associated with the data structure<br>
&nbsp; &nbsp; &nbsp; available for use in the implementation.<br>
<br>
&nbsp; &nbsp; &nbsp; Functions in the Domain box can use all of<br>
&nbsp; &nbsp; &nbsp; the definitions and axioms about the representation<br>=

&nbsp; &nbsp; &nbsp; (e.g. NonNegativeIntegers are always positive)<br>
<br>
&nbsp; C) contains local "spread" definitions and axioms<br>
&nbsp; &nbsp; &nbsp; &nbsp;that can be used in function proofs.<br>
<br>
&nbsp; &nbsp; &nbsp; For example, a "Square Matrix" domain would<br>
&nbsp; &nbsp; &nbsp; have local axioms that state that the matrix is<br>
&nbsp; &nbsp; &nbsp; always square. Thus, functions in that box could<br>
&nbsp; &nbsp; &nbsp; use these additional definitions and axioms in<br>
&nbsp; &nbsp; &nbsp; function proofs.<br>
<br>
&nbsp; D) contains local state. A "Square Matrix" domain<br>
&nbsp; &nbsp; &nbsp; &nbsp;would be constructed as a dependent type that<br>=

&nbsp; &nbsp; &nbsp; &nbsp;specified the size of the square (e.g. a 2x2<br>
&nbsp; &nbsp; &nbsp; &nbsp;matrix would have '2' as a dependent parameter.<b=
r>
<br>
&nbsp; E) contains implementations of inherited functions.<br>
<br>
&nbsp; &nbsp; &nbsp; &nbsp;A "Category" could have a signature for a GCD<br>=

&nbsp; &nbsp; &nbsp; &nbsp;function and the "Category" could have a default<=
br>
&nbsp; &nbsp; &nbsp; &nbsp;implementation. However, the "Domain" could<br>
&nbsp; &nbsp; &nbsp; &nbsp;have a locally more efficient implementation whic=
h<br>
&nbsp; &nbsp; &nbsp; &nbsp;overrides the inherited implementation.<br>
<br>
&nbsp; &nbsp; &nbsp; Axiom has about 20 GCD implementations that<br>
&nbsp; &nbsp; &nbsp; differ locally from the default in the category. They<b=
r>
&nbsp; &nbsp; &nbsp; use properties known locally to be more efficient.<br>
<br>
&nbsp; F) contains local function signatures.<br>
<br>
&nbsp; &nbsp; &nbsp; A "Domain" gives the user more and more unique<br>
&nbsp; &nbsp; &nbsp; functions. The signature have associated<br>
&nbsp; &nbsp; &nbsp; "pre- and post- conditions" that can be used<br>
&nbsp; &nbsp; &nbsp; as assumptions in the function proofs.<br>
<br>
&nbsp; &nbsp; &nbsp; Some of the user-available functions are only<br>
&nbsp; &nbsp; &nbsp; visible if the dependent type would allow them<br>
&nbsp; &nbsp; &nbsp; to exist. For example, a general Matrix domain<br>
&nbsp; &nbsp; &nbsp; would have fewer user functions that a Square<br>
&nbsp; &nbsp; &nbsp; Matrix domain.<br>
<br>
&nbsp; &nbsp; &nbsp; In addition, local "helper" functions need their<br>
&nbsp; &nbsp; &nbsp; own signatures that are not user visible.<br>
<br>
&nbsp; G) the function implementation for each signature.<br>
<br>
&nbsp; &nbsp; &nbsp; &nbsp;This is obviously where all the magic happens<br>=

<br>
&nbsp; H) the proof of each function.<br>
<br>
&nbsp; &nbsp; &nbsp; &nbsp;This is where I'm using LEAN.<br>
<br>
&nbsp; &nbsp; &nbsp; &nbsp;Every function has a proof. That proof can use<br=
>
&nbsp; &nbsp; &nbsp; &nbsp;all of the definitions and axioms inherited from<=
br>
&nbsp; &nbsp; &nbsp; &nbsp;the "Category", "Representation", the "Domain<br>=

&nbsp; &nbsp; &nbsp; &nbsp;Local", and the signature pre- and post-<br>
&nbsp; &nbsp; &nbsp; &nbsp;conditions.<br>
<br>
&nbsp; &nbsp;I) literature links. Algorithms must contain a link<br>
&nbsp; &nbsp; &nbsp; to at least one literature reference. Of course,<br>
&nbsp; &nbsp; &nbsp; since everything I do is a Literate Program<br>
&nbsp; &nbsp; &nbsp; this is obviously required. Knuth said so :-)<br>
<br>
<br>
LEAN ought to have "books" or "pamphlets" that<br>
bring together all of this information for a domain<br>
such as Square Matrices. That way a user can<br>
find all of the related ideas, available functions,<br>
and their corresponding proofs in one place.<br>
<br>
6) User level presentation.<br>
<br>
&nbsp; &nbsp; This is where the systems can differ significantly.<br>
&nbsp; &nbsp; Axiom and LEAN both have GCD but they use<br>
&nbsp; &nbsp; that for different purposes.<br>
<br>
&nbsp; &nbsp; I'm trying to connect LEAN's GCD and Axiom's GCD<br>
&nbsp; &nbsp; so there is a "computational mathematics" idea that<br>
&nbsp; &nbsp; allows the user to connect proofs and implementations.<br>
<br>
7) Trust<br>
<br>
Unlike everything else, computational mathematics<br>
can have proven code that gives various guarantees.<br>
<br>
I have been working on this aspect for a while.<br>
I refer to it as trust "down to the metal" The idea is<br>
that a proof of the GCD function and the implementation<br>
of the GCD function get packaged into the ELF format.<br>
(proof carrying code). When the GCD algorithm executes<br>
on the CPU, the GCD proof is run through the LEAN<br>
proof checker on an FPGA in parallel.<br>
<br>
(I just recently got a PYNQ Xilinx board [1] with a CPU<br>
and FPGA together. I'm trying to implement the LEAN<br>
proof checker on the FPGA).<br>
<br>
We are on the cusp of a revolution in computational<br>
mathematics. But the two pillars (proof and computer<br>
algebra) need to get know each other.<br>
<br>
Tim<br>
<br>
<br>
<br>
[0] Lamport, Leslie "Chapter on TLA+"<br>
in "Software Specification Methods"<br>
<a href=3D"https://www.springer.com/gp/book/9781852333539" rel=3D"noreferrer=
" target=3D"_blank">https://www.springer.com/gp/book/9781852333539</a><br>
(I no longer have CMU library access or I'd send you<br>
the book PDF)<br>
<br>
[1] <a href=3D"https://www.tul.com.tw/productspynq-z2.html" rel=3D"noreferre=
r" target=3D"_blank">https://www.tul.com.tw/productspynq-z2.html</a><br>
<br>
[2] <a href=3D"https://www.youtube.com/watch?v=3DdCuZkaaou0Q" rel=3D"norefer=
rer" target=3D"_blank">https://www.youtube.com/watch?v=3DdCuZkaaou0Q</a><br>=

<br>
[3] "ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE"<br>
<a href=3D"https://arxiv.org/pdf/1307.3091.pdf" rel=3D"noreferrer" target=3D=
"_blank">https://arxiv.org/pdf/1307.3091.pdf</a><br>
<br>
[4] ALICE Chatbot<br>
<a href=3D"http://www.scielo.org.mx/pdf/cys/v19n4/1405-5546-cys-19-04-00625.=
pdf" rel=3D"noreferrer" target=3D"_blank">http://www.scielo.org.mx/pdf/cys/v=
19n4/1405-5546-cys-19-04-00625.pdf</a><br>
<br>
[5] OPS5 User Manual<br>
<a href=3D"https://kilthub.cmu.edu/articles/journal_contribution/OPS5_user_s=
_manual/6608090/1" rel=3D"noreferrer" target=3D"_blank">https://kilthub.cmu.=
edu/articles/journal_contribution/OPS5_user_s_manual/6608090/1</a><br>
<br>
[6] Scott Fahlman "SCONE"<br>
<a href=3D"http://www.cs.cmu.edu/~sef/scone/" rel=3D"noreferrer" target=3D"_=
blank">http://www.cs.cmu.edu/~sef/scone/</a><br>
<br>
On 9/27/21, Tim Daly &lt;<a href=3D"mailto:[email protected]" target=3D"_bl=
ank">[email protected]</a>&gt; wrote:<br>
&gt; I have tried to maintain a list of names of people who have<br>
&gt; helped Axiom, going all the way back to the pre-Scratchpad<br>
&gt; days. The names are listed at the beginning of each book.<br>
&gt; I also maintain a bibliography of publications I've read or<br>
&gt; that have had an indirect influence on Axiom.<br>
&gt;<br>
&gt; Credit is "the coin of the realm". It is easy to share and wrong<br>
&gt; to ignore. It is especially damaging to those in Academia who<br>
&gt; are affected by credit and citations in publications.<br>
&gt;<br>
&gt; Apparently I'm not the only person who feels that way. The ACM<br>
&gt; Turing award seems to have ignored a lot of work:<br>
&gt;<br>
&gt; Scientific Integrity, the 2021 Turing Lecture, and the 2018 Turing<br>
&gt; Award for Deep Learning<br>
&gt; <a href=3D"https://people.idsia.ch/~juergen/scientific-integrity-turing=
-award-deep-learning.html" rel=3D"noreferrer" target=3D"_blank">https://peop=
le.idsia.ch/~juergen/scientific-integrity-turing-award-deep-learning.html</a=
><br>
&gt;<br>
&gt; I worked on an AI problem at IBM Research called Ketazolam.<br>
&gt; (<a href=3D"https://en.wikipedia.org/wiki/Ketazolam" rel=3D"noreferrer"=
 target=3D"_blank">https://en.wikipedia.org/wiki/Ketazolam</a>). The idea wa=
s to recognize<br>
&gt; and associated 3D chemical drawings with their drug counterparts.<br>
&gt; I used Rumelhart, and McClelland's books. These books contained<br>
&gt; quite a few ideas that seem to be "new and innovative" among the<br>
&gt; machine learning crowd... but the books are from 1987. I don't believe<=
br>
&gt; I've seen these books mentioned in any recent bibliography.<br>
&gt; <a href=3D"https://mitpress.mit.edu/books/parallel-distributed-processi=
ng-volume-1" rel=3D"noreferrer" target=3D"_blank">https://mitpress.mit.edu/b=
ooks/parallel-distributed-processing-volume-1</a><br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; On 9/27/21, Tim Daly &lt;<a href=3D"mailto:[email protected]" target=3D=
"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt; Greg Wilson asked "How Reliable is Scientific Software?"<br>
&gt;&gt; <a href=3D"https://neverworkintheory.org/2021/09/25/how-reliable-is=
-scientific-software.html" rel=3D"noreferrer" target=3D"_blank">https://neve=
rworkintheory.org/2021/09/25/how-reliable-is-scientific-software.html</a><br=
>
&gt;&gt;<br>
&gt;&gt; which is a really interesting read. For example"<br>
&gt;&gt;<br>
&gt;&gt;&nbsp; [Hatton1994], is now a quarter of a century old, but its conc=
lusions<br>
&gt;&gt; are still fresh. The authors fed the same data into nine commercial=
<br>
&gt;&gt; geophysical software packages and compared the results; they found<=
br>
&gt;&gt; that, "numerical disagreement grows at around the rate of 1% in<br>=

&gt;&gt; average absolute difference per 4000 fines of implemented code, and=
,<br>
&gt;&gt; even worse, the nature of the disagreement is nonrandom" (i.e., the=
<br>
&gt;&gt; authors of different packages make similar mistakes).<br>
&gt;&gt;<br>
&gt;&gt;<br>
&gt;&gt; On 9/26/21, Tim Daly &lt;<a href=3D"mailto:[email protected]" targ=
et=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt; I should note that the lastest board I've just unboxed<br>
&gt;&gt;&gt; (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD).<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; What makes it interesting is that it contains 2 hard<br>
&gt;&gt;&gt; core processors and an FPGA, connected by 9 paths<br>
&gt;&gt;&gt; for communication. The processors can be run<br>
&gt;&gt;&gt; independently so there is the possibility of a parallel<br>
&gt;&gt;&gt; version of some Axiom algorithms (assuming I had<br>
&gt;&gt;&gt; the time, which I don't).<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Previously either the hard (physical) processor was<br>
&gt;&gt;&gt; separate from the FPGA with minimal communication<br>
&gt;&gt;&gt; or the soft core processor had to be created in the FPGA<br>
&gt;&gt;&gt; and was much slower.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Now the two have been combined in a single chip.<br>
&gt;&gt;&gt; That means that my effort to run a proof checker on<br>
&gt;&gt;&gt; the FPGA and the algorithm on the CPU just got to<br>
&gt;&gt;&gt; the point where coordination is much easier.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Now all I have to do is figure out how to program this<br>
&gt;&gt;&gt; beast.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; There is no such thing as a simple job.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; On 9/26/21, Tim Daly &lt;<a href=3D"mailto:[email protected]" t=
arget=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt; I'm familiar with most of the traditional approaches<br>
&gt;&gt;&gt;&gt; like Theorema. The bibliography contains most of the<br>
&gt;&gt;&gt;&gt; more interesting sources. [0]<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; There is a difference between traditional approaches to<br>=

&gt;&gt;&gt;&gt; connecting computer algebra and proofs and my approach.<br>=

&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Proving an algorithm, like the GCD, in Axiom is hard.<br>
&gt;&gt;&gt;&gt; There are many GCDs (e.g. NNI vs POLY) and there<br>
&gt;&gt;&gt;&gt; are theorems and proofs passed at runtime in the<br>
&gt;&gt;&gt;&gt; arguments of the newly constructed domains. This<br>
&gt;&gt;&gt;&gt; involves a lot of dependent type theory and issues of<br>
&gt;&gt;&gt;&gt; compile time / runtime argument evaluation. The issues<br>
&gt;&gt;&gt;&gt; that arise are difficult and still being debated in the typ=
e<br>
&gt;&gt;&gt;&gt; theory community.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I am putting the definitions, theorems, and proofs (DTP)<br=
>
&gt;&gt;&gt;&gt; directly into the category/domain hierarchy. Each category<=
br>
&gt;&gt;&gt;&gt; will have the DTP specific to it. That way a commutative<br=
>
&gt;&gt;&gt;&gt; domain will inherit a commutative theorem and a<br>
&gt;&gt;&gt;&gt; non-commutative domain will not.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; Each domain will have additional DTPs associated with<br>
&gt;&gt;&gt;&gt; the domain (e.g. NNI vs Integer) as well as any DTPs<br>
&gt;&gt;&gt;&gt; it inherits from the category hierarchy. Functions in the<b=
r>
&gt;&gt;&gt;&gt; domain will have associated DTPs.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; A function to be proven will then inherit all of the releva=
nt<br>
&gt;&gt;&gt;&gt; DTPs. The proof will be attached to the function and<br>
&gt;&gt;&gt;&gt; both will be sent to the hardware (proof-carrying code).<br=
>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; The proof checker, running on a field programmable<br>
&gt;&gt;&gt;&gt; gate array (FPGA), will be checked at runtime in<br>
&gt;&gt;&gt;&gt; parallel with the algorithm running on the CPU<br>
&gt;&gt;&gt;&gt; (aka "trust down to the metal"). (Note that Intel<br>
&gt;&gt;&gt;&gt; and AMD have built CPU/FPGA combined chips,<br>
&gt;&gt;&gt;&gt; currently only available in the cloud.)<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I am (slowly) making progress on the research.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I have the hardware and nearly have the proof<br>
&gt;&gt;&gt;&gt; checker from LEAN running on my FPGA.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I'm in the process of spreading the DTPs from<br>
&gt;&gt;&gt;&gt; LEAN across the category/domain hierarchy.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; The current Axiom build extracts all of the functions<br>
&gt;&gt;&gt;&gt; but does not yet have the DTPs.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I have to restructure the system, including the compiler<br=
>
&gt;&gt;&gt;&gt; and interpreter to parse and inherit the DTPs. I<br>
&gt;&gt;&gt;&gt; have some of that code but only some of the code<br>
&gt;&gt;&gt;&gt; has been pushed to the repository (volume 15) but<br>
&gt;&gt;&gt;&gt; that is rather trivial, out of date, and incomplete.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; I'm clearly not smart enough to prove the Risch<br>
&gt;&gt;&gt;&gt; algorithm and its associated machinery but the needed<br>
&gt;&gt;&gt;&gt; definitions and theorems will be available to someone<br>
&gt;&gt;&gt;&gt; who wants to try.<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; [0] <a href=3D"https://github.com/daly/PDFS/blob/master/boo=
kvolbib.pdf" rel=3D"noreferrer" target=3D"_blank">https://github.com/daly/PD=
FS/blob/master/bookvolbib.pdf</a><br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt; On 8/19/21, Tim Daly &lt;<a href=3D"mailto:[email protected]=
om" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt; =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; REVIEW (Axiom on WSL2 Windows)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; So the steps to run Axiom from a Windows desktop<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 1 Windows) install XMing on Windows for X11 server<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; <a href=3D"http://www.straightrunning.com/XmingNotes/" r=
el=3D"noreferrer" target=3D"_blank">http://www.straightrunning.com/XmingNote=
s/</a><br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 2 WSL2) Install Axiom in WSL2<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; sudo apt install axiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 3 WSL2) modify /usr/bin/axiom to fix the bug:<br>
&gt;&gt;&gt;&gt;&gt; (someone changed the axiom startup script.<br>
&gt;&gt;&gt;&gt;&gt; It won't work on WSL2. I don't know who or<br>
&gt;&gt;&gt;&gt;&gt; how to get it fixed).<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; sudo emacs /usr/bin/axiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; (split the line into 3 and add quote marks)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; export SPADDEFAULT=3D/usr/local/axiom/mnt/linux<br>
&gt;&gt;&gt;&gt;&gt; export AXIOM=3D/usr/lib/axiom-20170501<br>
&gt;&gt;&gt;&gt;&gt; export "PATH=3D/usr/lib/axiom-20170501/bin:$PATH"<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 4 WSL2) create a .axiom.input file to include startup c=
mds:<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; emacs .axiom.input<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; )cd "/mnt/c/yourpath"<br>
&gt;&gt;&gt;&gt;&gt; )sys pwd<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 5 WSL2) create a "myaxiom" command that sets the<br>
&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; &nbsp;DISPLAY variable and starts axiom<br=
>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; emacs myaxiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; #! /bin/bash<br>
&gt;&gt;&gt;&gt;&gt; export DISPLAY=3D:0.0<br>
&gt;&gt;&gt;&gt;&gt; axiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 6 WSL2) put it in the /usr/bin directory<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; chmod +x myaxiom<br>
&gt;&gt;&gt;&gt;&gt; sudo cp myaxiom /usr/bin/myaxiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 7 WINDOWS) start the X11 server<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; (XMing XLaunch Icon on your desktop)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 8 WINDOWS) run myaxiom from PowerShell<br>
&gt;&gt;&gt;&gt;&gt; (this should start axiom with graphics available)<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; wsl myaxiom<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 8 WINDOWS) make a PowerShell desktop<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; <a href=3D"https://superuser.com/questions/886951/run-p=
owershell-script-when-you-open-powershell" rel=3D"noreferrer" target=3D"_bla=
nk">https://superuser.com/questions/886951/run-powershell-script-when-you-op=
en-powershell</a><br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; On 8/13/21, Tim Daly &lt;<a href=3D"mailto:axiomcas@gma=
il.com" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt; A great deal of thought is directed toward making t=
he SANE version<br>
&gt;&gt;&gt;&gt;&gt;&gt; of Axiom as flexible as possible, decoupling mechan=
ism from theory.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; An interesting publication by Brian Cantwell Smith [=
0], "Reflection<br>
&gt;&gt;&gt;&gt;&gt;&gt; and Semantics in LISP" seems to contain interesting=
 ideas related<br>
&gt;&gt;&gt;&gt;&gt;&gt; to our goal. Of particular interest is the ability t=
o reason about<br>
&gt;&gt;&gt;&gt;&gt;&gt; and<br>
&gt;&gt;&gt;&gt;&gt;&gt; perform self-referential manipulations. In a depend=
ently-typed<br>
&gt;&gt;&gt;&gt;&gt;&gt; system it seems interesting to be able "adapt" code=
 to handle<br>
&gt;&gt;&gt;&gt;&gt;&gt; run-time computed arguments to dependent functions.=
 The abstract:<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; "We show how a computational system ca=
n be constructed to<br>
&gt;&gt;&gt;&gt;&gt;&gt; "reason",<br>
&gt;&gt;&gt;&gt;&gt;&gt; effectively<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; and consequentially, about its own inf=
erential processes. The<br>
&gt;&gt;&gt;&gt;&gt;&gt; analysis proceeds in two<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; parts. First, we consider the general q=
uestion of computational<br>
&gt;&gt;&gt;&gt;&gt;&gt; semantics, rejecting<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; traditional approaches, and arguing th=
at the declarative and<br>
&gt;&gt;&gt;&gt;&gt;&gt; procedural aspects of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; computational symbols (what they stand=
 for, and what behaviour<br>
&gt;&gt;&gt;&gt;&gt;&gt; they<br>
&gt;&gt;&gt;&gt;&gt;&gt; engender) should be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; analysed independently, in order that t=
hey may be coherently<br>
&gt;&gt;&gt;&gt;&gt;&gt; related. Second, we<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; investigate self-referential behavior i=
n computational processes,<br>
&gt;&gt;&gt;&gt;&gt;&gt; and show how to embed an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; effective procedural model of a comput=
ational calculus within that<br>
&gt;&gt;&gt;&gt;&gt;&gt; calculus (a model not<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; unlike a meta-circular interpreter, bu=
t connected to the<br>
&gt;&gt;&gt;&gt;&gt;&gt; fundamental operations of the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; machine in such a way as to provide, a=
t any point in a<br>
&gt;&gt;&gt;&gt;&gt;&gt; computation,<br>
&gt;&gt;&gt;&gt;&gt;&gt; fully articulated<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; descriptions of the state of that comp=
utation, for inspection and<br>
&gt;&gt;&gt;&gt;&gt;&gt; possible modification). In<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; terms of the theories that result from=
 these investigations, we<br>
&gt;&gt;&gt;&gt;&gt;&gt; present a general architecture<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; for procedurally reflective processes,=
 able to shift smoothly<br>
&gt;&gt;&gt;&gt;&gt;&gt; between dealing with a given<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; subject domain, and dealing with their=
 own reasoning processes<br>
&gt;&gt;&gt;&gt;&gt;&gt; over<br>
&gt;&gt;&gt;&gt;&gt;&gt; that domain.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; An instance of the general solution is=
 worked out in the context<br>
&gt;&gt;&gt;&gt;&gt;&gt; of<br>
&gt;&gt;&gt;&gt;&gt;&gt; an applicative<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; language. Specifically, we present thr=
ee successive dialects of<br>
&gt;&gt;&gt;&gt;&gt;&gt; LISP: 1-LISP, a distillation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; current practice, for comparison purpo=
ses; 2-LISP, a dialect<br>
&gt;&gt;&gt;&gt;&gt;&gt; constructed in terms of our<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; rationalised semantics, in which the c=
oncept of evaluation is<br>
&gt;&gt;&gt;&gt;&gt;&gt; rejected in favour of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; independent notions of simplification a=
nd reference, and in which<br>
&gt;&gt;&gt;&gt;&gt;&gt; the respective categories<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; of notation, structure, semantics, and=
 behaviour are strictly<br>
&gt;&gt;&gt;&gt;&gt;&gt; aligned; and 3-LISP, an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; extension of 2-LISP endowed with refle=
ctive powers."<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; Axiom SANE builds dependent types on the fly. The a=
bility to access<br>
&gt;&gt;&gt;&gt;&gt;&gt; both the refection<br>
&gt;&gt;&gt;&gt;&gt;&gt; of the tower of algebra and the reflection of the t=
ower of proofs at<br>
&gt;&gt;&gt;&gt;&gt;&gt; the time of construction<br>
&gt;&gt;&gt;&gt;&gt;&gt; makes the construction of a new domain or specific a=
lgorithm easier<br>
&gt;&gt;&gt;&gt;&gt;&gt; and more general.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; This is of particular interest because one of the e=
fforts is to build<br>
&gt;&gt;&gt;&gt;&gt;&gt; "all the way down to the<br>
&gt;&gt;&gt;&gt;&gt;&gt; metal". If each layer is constructed on top of prev=
ious proven layers<br>
&gt;&gt;&gt;&gt;&gt;&gt; and the new layer<br>
&gt;&gt;&gt;&gt;&gt;&gt; can "reach below" to lower layers then the tower of=
 layers can be<br>
&gt;&gt;&gt;&gt;&gt;&gt; built without duplication.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; [0], Smith, Brian Cantwell "Reflection and Semantic=
s in LISP"<br>
&gt;&gt;&gt;&gt;&gt;&gt; POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLA=
N<br>
&gt;&gt;&gt;&gt;&gt;&gt; ymposium on Principles of programming languagesJanu=
ary 1<br>
&gt;&gt;&gt;&gt;&gt;&gt; 984 Pages 23=E2=80=9335<a href=3D"https://doi.org/1=
0.1145/800017.800513" rel=3D"noreferrer" target=3D"_blank">https://doi.org/1=
0.1145/800017.800513</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; On 6/29/21, Tim Daly &lt;<a href=3D"mailto:axiomcas=
@gmail.com" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Having spent time playing with hardware it is p=
erfectly clear that<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; future computational mathematics efforts need t=
o adapt to using<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; parallel processing.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; I've spent a fair bit of time thinking about st=
ructuring Axiom to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; be parallel. Most past efforts have tried to fo=
cus on making a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; particular algorithm parallel, such as a matrix=
 multiply.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; But I think that it might be more effective to m=
ake each domain<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; run in parallel. A computation crosses multiple=
 domains so a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; particular computation could involve multiple p=
arallel copies.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; For example, computing the Cylindrical Algebrai=
c Decomposition<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; could recursively decompose the plane. Indeed, a=
ny tree-recursive<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; algorithm could be run in parallel "in the larg=
e" by creating new<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; running copies of the domain for each sub-probl=
em.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So the question becomes, how does one manage th=
is?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; A similar problem occurs in robotics where one c=
ould have multiple<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; wheels, arms, propellers, etc. that need to act=
 independently but<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; in coordination.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; The robot solution uses ROS2. The three ideas a=
re ROSCORE,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; TOPICS with publish/subscribe, and SERVICES wit=
h request/response.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; These are communication paths defined between p=
rocesses.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; ROS2 has a "roscore" which is basically a phone=
book of "topics".<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can create or look up the current a=
ctive topics. eq:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; rosnode list<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; TOPICS:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can PUBLISH a topic (which is basic=
ally a typed data<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure), e.g the topic /hw with the String d=
ata "Hello World".<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; eg:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; rostopic pub /hw std_msgs/String "=
Hello, World"<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can SUBSCRIBE to a topic, such as /=
hw, and get a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; copy of the data.&nbsp; eg:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&nbsp; &nbsp; rostopic echo /hw&nbsp; &nbsp;=3D=3D=
&gt; "Hello, World"<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Publishers talk, subscribers listen.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; SERVICES:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can make a REQUEST of a SERVICE and=
 get a RESPONSE.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; This is basically a remote function call.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom in parallel?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So domains could run, each in its own process. I=
t could provide<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; services, one for each function. Any other proc=
ess could request<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; a computation and get the result as a response.=
 Domains could<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; request services from other domains, either wai=
ting for responses<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; or continuing while the response is being compu=
ted.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; The output could be sent anywhere, to a termina=
l, to a browser,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; to a network, or to another process using the p=
ublish/subscribe<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; protocol, potentially all at the same time sinc=
e there can be many<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; subscribers to a topic.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Available domains could be dynamically added by=
 announcing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; themselves as new "topics" and could be dynamic=
ally looked-up<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; at runtime.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; This structure allows function-level / domain-l=
evel parallelism.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is very effective in the robot world and I t=
hink it might be a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; good structuring mechanism to allow computation=
al mathematics<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; to take advantage of multiple processors in a d=
isciplined fashion.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom has a thousand domains and each could run=
 on its own core.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; In addition. notice that each domain is indepen=
dent of the others.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So if we want to use BLAS Fortran code, it coul=
d just be another<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; service node. In fact, any "foreign function" c=
ould transparently<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; cooperate in a distributed Axiom.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Another key feature is that proofs can be "by n=
ode".<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 6/5/21, Tim Daly &lt;<a href=3D"mailto:axiom=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom is based on first-class dependent typ=
es. Deciding when<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; two types are equivalent may involve comput=
ation. See<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Christiansen, David Thrane "Checking Depend=
ent Types with<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Normalization by Evaluation" (2019)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; This puts an interesting constraint on buil=
ding types. The<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; constructed types has to export a function t=
o decide if a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; given type is "equivalent" to itself.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The notion of "equivalence" might involve c=
ategory ideas<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of natural transformation and univalence. S=
igh.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; That's an interesting design point.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 5/5/21, Tim Daly &lt;<a href=3D"mailto:a=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is interesting that programmer's eye=
s and expectations adapt<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to the tools they use. For instance, I u=
se emacs and expect to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; work directly in files and multiple buf=
fers. When I try to use one<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the many IDE tools I find they tend t=
o "get in the way". I<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; already<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; know or can quickly find whatever they t=
ry to tell me. If you use<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; IDE you probably find emacs "too sparse=
" for programming.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Recently I've been working in a sparse p=
rogramming environment.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I'm exploring the question of running a=
 proof checker in an FPGA.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The FPGA development tools are painful a=
t best and not intuitive<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; since you SEEM to be programming but yo=
u're actually describing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; hardware gates, connections, and timing=
. This is an environment<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; where everything happens all-at-once an=
d all-the-time (like the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; circuits in your computer). It is the "=
assembly language of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; circuits".<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Naturally, my eyes have adapted to this=
 rather raw level.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; That said, I'm normally doing literate p=
rogramming all the time.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; My typical file is a document which is a=
 mixture of latex and<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; lisp.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is something of a shock to return to=
 that world. It is clear<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; why<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; people who program in Python find lisp t=
o be a "sea of parens".<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Yet as a lisp programmer, I don't even s=
ee the parens, just code.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It takes a few minutes in a literate do=
cument to adapt vision to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; see the latex / lisp combination as nat=
ural. The latex markup,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; like the lisp parens, eventually just d=
isappears. What remains<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; is just lisp and natural language text.=
<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; This seems painful at first but eyes qu=
ickly adapt. The upside<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; is that there is always a "finished" do=
cument that describes the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; state of the code. The overhead of writ=
ing a paragraph to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; describe a new function or change a par=
agraph to describe the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; changed function is very small.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Using a Makefile I latex the document t=
o generate a current PDF<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and then I extract, load, and execute t=
he code. This loop catches<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; errors in both the latex and the source=
 code. Keeping an open file<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; my pdf viewer shows all of the changes i=
n the document after every<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; run of make. That way I can edit the bo=
ok as easily as the code.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Ultimately I find that writing the book=
 while writing the code is<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; more productive. I don't have to rememb=
er why I wrote something<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; since the explanation is already there.=
<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; We all have our own way of programming a=
nd our own tools.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; But I find literate programming to be a=
 real advance over IDE<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; style programming and "raw code" progra=
mming.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 2/27/21, Tim Daly &lt;<a href=3D"mai=
lto:[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<=
br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The systems I use have the interest=
ing property of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; "Living within the compiler".<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Lisp, Forth, Emacs, and other syste=
ms that present themselves<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; through the Read-Eval-Print-Loop (R=
EPL) allow the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; ability to deeply interact with the=
 system, shaping it to your<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; need.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; My current thread of study is softw=
are architecture. See<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href=3D"https://www.youtube.com/=
watch?v=3DW2hagw1VhhI&amp;feature=3Dyoutu.be" rel=3D"noreferrer" target=3D"_=
blank">https://www.youtube.com/watch?v=3DW2hagw1VhhI&amp;feature=3Dyoutu.be<=
/a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and <a href=3D"https://www.georgefa=
irbanks.com/videos/" rel=3D"noreferrer" target=3D"_blank">https://www.george=
fairbanks.com/videos/</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; My current thinking on SANE involve=
s the ability to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; dynamically define categories, repr=
esentations, and functions<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; along with "composition functions" t=
hat permits choosing a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; combination at the time of use.<br>=

&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; You might want a domain for handlin=
g polynomials. There are<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a lot of choices, depending on your=
 use case. You might want<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; different representations. For exam=
ple, you might want dense,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; sparse, recursive, or "machine comp=
atible fixnums" (e.g. to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; interface with C code). If these do=
n't exist it ought to be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; possible<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to create them. Such "lego-like" bu=
ilding blocks require careful<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; thought about creating "fully facto=
red" objects.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Given that goal, the traditional ba=
rrier of "compiler" vs<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; "interpreter"<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; does not seem useful. It is better t=
o "live within the compiler"<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; which<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; gives the ability to define new thi=
ngs "on the fly".<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Of course, the SANE compiler is goi=
ng to want an associated<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; proof of the functions you create a=
long with the other parts<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; such as its category hierarchy and r=
epresentation properties.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; There is no such thing as a simple j=
ob. :-)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 2/18/21, Tim Daly &lt;<a href=3D=
"mailto:[email protected]" target=3D"_blank">[email protected]</a>&gt; wro=
te:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The Axiom SANE compiler / inter=
preter has a few design points.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; 1) It needs to mix interpreted a=
nd compiled code in the same<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; function.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; SANE allows dynamic constructio=
n of code as well as dynamic type<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; construction at runtime. Both o=
f these can occur in a runtime<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; object.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; So there is potentially a mixtu=
re of interpreted and compiled<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; code.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; 2) It needs to perform type res=
olution at compile time without<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; overhead<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; where possible. Since this is n=
ot always possible there needs to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a "prefix thunk" that will perf=
orm the resolution. Trivially,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; for<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; example,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; if we have a + function we need=
 to type-resolve the arguments.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; However, if we can prove at com=
pile time that the types are both<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; bounded-NNI and the result is b=
ounded-NNI (i.e. fixnum in lisp)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; then we can inline a call to + a=
t runtime. If not, we might have<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; + applied to NNI and POLY(FLOAT=
), which requires a thunk to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; resolve types. The thunk could e=
ven "specialize and compile"<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the code before executing it.<b=
r>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It turns out that the Forth imp=
lementation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; "threaded-interpreted"<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; languages model provides an eff=
icient and effective way to do<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; this.[0]<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Type resolution can be "inserte=
d" in intermediate thunks.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The model also supports dynamic=
 overloading and tail recursion.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Combining high-level CLOS code w=
ith low-level threading gives an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; easy to understand and robust d=
esign.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; [0] Loeliger, R.G. "Threaded In=
terpretive Languages" (1981)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; ISBN 0-07-038360-X<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 2/5/21, Tim Daly &lt;<a href=
=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>&gt; w=
rote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I've worked hard to make Ax=
iom depend on almost no other<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; tools so that it would not g=
et caught by "code rot" of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; libraries.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; However, I'm also trying to=
 make the new SANE version much<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; easier to understand and de=
bug.To that end I've been<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; experimenting<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; with some ideas.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; It should be possible to vi=
ew source code, of course. But the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; source<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; code is not the only, nor p=
ossibly the best, representation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; ideas.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In particular, source code g=
ets compiled into data structures.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; these data structures reall=
y are a graph of related structures.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; For example, looking at the=
 gcd function from NNI, there is the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; representation of the gcd f=
unction itself. But there is also a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; that is the REP (and, in th=
e new system, is separate from the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; domain).<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Further, there are associat=
ed specification and proof<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structures.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Even<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; further, the domain inherit=
s the category structures, and from<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; those<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; it<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; inherits logical axioms and=
 definitions through the proof<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Clearly the gcd function is=
 a node in a much larger graph<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; When trying to decide why c=
ode won't compile it would be useful<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; be able to see and walk the=
se structures. I've thought about<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; using<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; browser but browsers are to=
o weak. Either everything has to be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; "in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; single tab to show the grap=
h" or "the nodes of the graph are in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; different<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; tabs". Plus, constructing d=
ynamic graphs that change as the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; software<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; changes (e.g. by loading a n=
ew spad file or creating a new<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; function)<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; represents the huge problem=
 of keeping the browser "in sync<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; with<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom workspace". So someth=
ing more dynamic and embedded is<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; needed.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom source gets compiled i=
nto CLOS data structures. Each of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; these<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; new SANE structures has an a=
ssociated surface representation,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; so<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; they<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; can be presented in user-fr=
iendly form.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Also, since Axiom is litera=
te software, it should be possible<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; look<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; at<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the code in its literate fo=
rm with the surrounding explanation.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Essentially we'd like to ha=
ve the ability to "deep dive" into<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Axiom<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; workspace, not only for deb=
ugging, but also for understanding<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; what<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; functions are used, where t=
hey come from, what they inherit,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; how they are used in a comp=
utation.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; To that end I'm looking at u=
sing McClim, a lisp windowing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; system.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Since the McClim windows wo=
uld be part of the lisp image, they<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; have<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; access to display (and modi=
fy) the Axiom workspace at all<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; times.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The only hesitation is that=
 McClim uses quicklisp and drags in<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; lot<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of other subsystems. It's a=
ll lisp, of course.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; These ideas aren't new. The=
y were available on Symbolics<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; machines,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a truly productive platform=
 and one I sorely miss.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 1/19/21, Tim Daly &lt;<a=
 href=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>=
&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Also of interest is the=
 talk<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; "The Unreasonable Effec=
tiveness of Dynamic Typing for<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Practical<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Programs"<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href=3D"https://vime=
o.com/74354480" rel=3D"noreferrer" target=3D"_blank">https://vimeo.com/74354=
480</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; which questions whether=
 static typing really has any benefit.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; On 1/19/21, Tim Daly &l=
t;<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]=
</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Peter Naur wrote an=
 article of interest:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href=3D"http://p=
ages.cs.wisc.edu/~remzi/Naur.pdf" rel=3D"noreferrer" target=3D"_blank">http:=
//pages.cs.wisc.edu/~remzi/Naur.pdf</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In particular, it m=
irrors my notion that Axiom needs<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to embrace literate=
 programming so that the "theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the problem" is p=
resented as well as the "theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the solution". I=
 quote the introduction:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; This article is, to=
 my mind, the most accurate account<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of what goes on in d=
esigning and coding a program.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I refer to it regul=
arly when discussing how much<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; documentation to cr=
eate, how to pass along tacit<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; knowledge, and the v=
alue of the XP's metaphor-setting<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; exercise. It also p=
rovides a way to examine a methodolgy's<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; economic structure.=
<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; In the article, whi=
ch follows, note that the quality of the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; designing programme=
r's work is related to the quality of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the match between h=
is theory of the problem and his theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the solution. No=
te that the quality of a later<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; programmer's<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; work is related to t=
he match between his theories and the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; previous programmer=
's theories.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Using Naur's ideas,=
 the designer's job is not to pass along<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; "the design" but to=
 pass along "the theories" driving the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; design.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The latter goal is m=
ore useful and more appropriate. It also<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; highlights that kno=
wledge of the theory is tacit in the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; owning,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; so passing along th=
e thoery requires passing along both<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; explicit<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and tacit knowledge=
.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Tim<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;<br>
&gt;&gt;<br>
&gt;<br>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>
</div></blockquote></div></body></html>=

--Apple-Mail-18CBE148-0FFC-47D9-9D95-5D7EFE73CB6B--