Re: Axiom musings...

--000000000000cf249d05da14f883
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

Axiom has an awkward 'attributes' category structure.

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'.

Tim


On Fri, Mar 11, 2022 at 9:46 AM Tim Daly <[email protected]> wrote:

> The github lockout continues...
>
> I'm spending some time adding examples to source code.
>
> 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:
>
>   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)
>
>
>
> Later, in the interpreter we see:
>
>
>
>
> )d op strongGenerators
>
>   There is one exposed function called strongGenerators :
>       [1] PermutationGroup(D2) -> List(Permutation(D2)) from
>                PermutationGroup(D2)
>                  if D2 has SETCAT
>
>   Examples of strongGenerators from PermutationGroup
>
>   S:List(Integer) :=3D [1,2,3,4]
>   G :=3D symmetricGroup(S)
>   strongGenerators(G)
>
>
>
>
> 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.
>
> These "example" functions are run at build time when
> the make command looks like
>     make TESTSET=3Dalltests
>
> I hope to add this documentation to all Axiom functions.
>
> 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.
>
> Tim
>
>
>
>
> On Fri, Feb 25, 2022 at 6:05 PM Tim Daly <[email protected]> wrote:
>
>> It turns out that creating SPAD-looking output is trivial
>> in Common Lisp. Each class can have a custom print
>> routine so signatures and ++ comments can each be
>> printed with their own format.
>>
>> 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.
>>
>> Internally, however, it will all be Common Lisp.
>>
>> 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.
>>
>> Tim
>>
>>
>> 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.
>>>
>>> I've decided that the SANE version of Axiom will be
>>> 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.
>>>
>>> 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.
>>>
>>> The input / output mathematics will remain the same.
>>> Indeed, with the new generalizations for first-class
>>> dependent types it will be more general.
>>>
>>> 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".
>>>
>>> Research is the whole point of Axiom.
>>>
>>> Tim
>>>
>>>
>>>
>>> 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
>>>>
>>>> Axiom will begin to die the day I stop working on it.
>>>>
>>>> However, proving Axiom correct "down to the metal", is fundamental.
>>>> It will merge computer algebra and logic, spawning years of new
>>>> research.
>>>>
>>>> Work on fundamental problems.
>>>>
>>>> Tim
>>>>
>>>>
>>>> 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.
>>>>>
>>>>> There is an idea called the "writer monad" [0], usually
>>>>> 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.
>>>>>
>>>>> For those unfamiliar with the monad idea, the best explanation
>>>>> I've found is this video [1].
>>>>>
>>>>> Tim
>>>>>
>>>>> [0] Deriving the writer monad from first principles
>>>>> https://williamyaoh.com/posts/2020-07-26-deriving-writer-monad.html
>>>>>
>>>>> [1] The Absolute Best Intro to Monads for Software Engineers
>>>>> https://www.youtube.com/watch?v=3DC2w45qRc3aU
>>>>>
>>>>> On Mon, Dec 13, 2021 at 12:30 AM Tim Daly <[email protected]> wrote:
>>>>>
>>>>>> ...(snip)...
>>>>>>
>>>>>> 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.
>>>>>>
>>>>>> Whether you USE the discipline afforded is the real question.
>>>>>>
>>>>>> 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".
>>>>>>
>>>>>> 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.)
>>>>>>
>>>>>> 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.
>>>>>>
>>>>>> Making proof technology work at compile time is hard.
>>>>>> (Worse yet, LEAN is a moving target. Sigh.)
>>>>>>
>>>>>>
>>>>>>
>>>>>> On Thu, Nov 25, 2021 at 9:43 AM Tim Daly <[email protected]> wrote:
>>>>>>
>>>>>>>
>>>>>>> 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.
>>>>>>>
>>>>>>> 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).
>>>>>>>
>>>>>>> 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.
>>>>>>>
>>>>>>> There is a bit of a disconnect, though. The GCD code is compiled
>>>>>>> machine code but the proof is LEAN-level.
>>>>>>>
>>>>>>> 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.
>>>>>>>
>>>>>>> What does it mean to "compile a proof to the machine code level"?
>>>>>>>
>>>>>>> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
>>>>>>> To quote from the article [0]:
>>>>>>>
>>>>>>>    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.
>>>>>>>
>>>>>>>    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.
>>>>>>>
>>>>>>> This gives a technique for "compiling the proof" down the the machi=
ne
>>>>>>> code level. Ideally, the compiler would have judgments for each ste=
p
>>>>>>> of
>>>>>>> the compilation so that each compile step has a justification. I
>>>>>>> don't
>>>>>>> know of any compiler that does this yet. (References welcome).
>>>>>>>
>>>>>>> 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).
>>>>>>>
>>>>>>> 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 FPG=
A
>>>>>>> ensures the proof is not violated, instruction by instruction.
>>>>>>>
>>>>>>> (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 bette=
r
>>>>>>> but
>>>>>>> it is still a "misty fog" for me.)
>>>>>>>
>>>>>>> The result is proven code "down to the metal".
>>>>>>>
>>>>>>> Tim
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>> [0]
>>>>>>> https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/i=
ndex-seo.php/ACL2____MILAWA
>>>>>>>
>>>>>>> On Thu, Nov 25, 2021 at 6:05 AM Tim Daly <[email protected]> wrote=
:
>>>>>>>
>>>>>>>>
>>>>>>>> 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.
>>>>>>>>
>>>>>>>> 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).
>>>>>>>>
>>>>>>>> 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.
>>>>>>>>
>>>>>>>> There is a bit of a disconnect, though. The GCD code is compiled
>>>>>>>> machine code but the proof is LEAN-level.
>>>>>>>>
>>>>>>>> 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.
>>>>>>>>
>>>>>>>> What does it mean to "compile a proof to the machine code level"?
>>>>>>>>
>>>>>>>> The Milawa effort (Myre14.pdf) does incremental proofs in layers.
>>>>>>>> To quote from the article [0]:
>>>>>>>>
>>>>>>>>    We begin with a simple proof checker, call it A, which is short
>>>>>>>>    enough to verify by the ``social process'' of mathematics -- an=
d
>>>>>>>>   more recently with a theorem prover for a more expressive logic.
>>>>>>>>
>>>>>>>>    We then develop a series of increasingly powerful proof checker=
s,
>>>>>>>>   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.
>>>>>>>>
>>>>>>>> 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).
>>>>>>>>
>>>>>>>> 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).
>>>>>>>>
>>>>>>>> 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. Th=
e
>>>>>>>> pair is sent to the CPU/FPGA and, while the algorithm runs, the FP=
GA
>>>>>>>> ensures the proof is not violated, instruction by instruction.
>>>>>>>>
>>>>>>>> (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.)
>>>>>>>>
>>>>>>>> The result is proven code "down to the metal".
>>>>>>>>
>>>>>>>> Tim
>>>>>>>>
>>>>>>>>
>>>>>>>>
>>>>>>>> [0]
>>>>>>>> https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/=
index-seo.php/ACL2____MILAWA
>>>>>>>>
>>>>>>>> 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.
>>>>>>>>>
>>>>>>>>> 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.
>>>>>>>>>
>>>>>>>>> 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.
>>>>>>>>>
>>>>>>>>> There is "The Metaobject Protocol" (MOP)
>>>>>>>>>
>>>>>>>>> https://www.amazon.com/Art-Metaobject-Protocol-Gregor-Kiczales/dp=
/0262610744
>>>>>>>>> which encourages a three-level process. The language designer
>>>>>>>>> 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 proble=
m.
>>>>>>>>>
>>>>>>>>> A simple paper on the subject is "Metaobject Protocols"
>>>>>>>>> https://users.cs.duke.edu/~vahdat/ps/mop.pdf
>>>>>>>>>
>>>>>>>>> Tim
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> 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)
>>>>>>>>>>
>>>>>>>>>> which led to watching "Strange Dreams of Stranger Loops" by Will
>>>>>>>>>> Byrd
>>>>>>>>>> https://www.youtube.com/watch?v=3DAffW-7ika0E
>>>>>>>>>>
>>>>>>>>>> Will referenced a PhD Thesis by Jon Doyle
>>>>>>>>>> "A Model for Deliberation, Action, and Introspection"
>>>>>>>>>>
>>>>>>>>>> I also read the thesis by J.C.G. Sturdy
>>>>>>>>>> "A Lisp through the Looking Glass"
>>>>>>>>>>
>>>>>>>>>> Self-replication requires the ability to manipulate your own
>>>>>>>>>> representation in such a way that changes to that representation
>>>>>>>>>> will change behavior.
>>>>>>>>>>
>>>>>>>>>> This leads to two thoughts in the SANE research.
>>>>>>>>>>
>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>>> 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.
>>>>>>>>>>
>>>>>>>>>> Tim
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> On Thu, Oct 21, 2021 at 9:50 AM Tim Daly <[email protected]>
>>>>>>>>>> wrote:
>>>>>>>>>>
>>>>>>>>>>> So the current struggle involves the categories in Axiom.
>>>>>>>>>>>
>>>>>>>>>>> The categories and domains constructed using categories
>>>>>>>>>>> are dependent types. When are dependent types "equal"?
>>>>>>>>>>> Well, hummmm, that depends on the arguments to the
>>>>>>>>>>> constructor.
>>>>>>>>>>>
>>>>>>>>>>> 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
>>>>>>>>>>> arguments at compile time (well, "construction time" as
>>>>>>>>>>> there isn't really a compiler / interpreter separation anymore.=
)
>>>>>>>>>>>
>>>>>>>>>>> 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.
>>>>>>>>>>>
>>>>>>>>>>> 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
>>>>>>>>>>> connect these assumptions to the groupoid structure.
>>>>>>>>>>>
>>>>>>>>>>> My brain hurts.
>>>>>>>>>>>
>>>>>>>>>>> Tim
>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> On Mon, Oct 18, 2021 at 2:00 AM Tim Daly <[email protected]>
>>>>>>>>>>> wrote:
>>>>>>>>>>>
>>>>>>>>>>>> "Birthing Computational Mathematics"
>>>>>>>>>>>>
>>>>>>>>>>>> The Axiom SANE project is difficult at a very fundamental
>>>>>>>>>>>> level. The title "SANE" was chosen due to the various
>>>>>>>>>>>> words found in a thesuarus... "rational", "coherent",
>>>>>>>>>>>> "judicious" and "sound".
>>>>>>>>>>>>
>>>>>>>>>>>> These are very high level, amorphous ideas. But so is
>>>>>>>>>>>> the design of 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).
>>>>>>>>>>>>
>>>>>>>>>>>> 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?
>>>>>>>>>>>>
>>>>>>>>>>>> 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.
>>>>>>>>>>>>
>>>>>>>>>>>> Unlike building design and contruction, however, there
>>>>>>>>>>>> are almost no constraints to use as guides. Alexander
>>>>>>>>>>>> quotes Plato's Phaedrus:
>>>>>>>>>>>>
>>>>>>>>>>>>   "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
>>>>>>>>>>>>    carver might."
>>>>>>>>>>>>
>>>>>>>>>>>> Lisp, which has been called "clay for the mind" can
>>>>>>>>>>>> build virtually anything that can be thought. The
>>>>>>>>>>>> "joints" are also "of one's choosing" so one is
>>>>>>>>>>>> both carver and "nature".
>>>>>>>>>>>>
>>>>>>>>>>>> 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.
>>>>>>>>>>>>
>>>>>>>>>>>> Tim
>>>>>>>>>>>>
>>>>>>>>>>>> [0] Alexander, Christopher "Notes on the Synthesis
>>>>>>>>>>>> of Form" Harvard University Press 1964
>>>>>>>>>>>> ISBN 0-674-62751-2
>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> "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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Notation matters and is not widely common.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I have no idea how to extend any system to deal with
>>>>>>>>>>>>> even undergraduate mathematics parsing.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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 :-)
>>>>>>>>>>>>>
>>>>>>>>>>>>> A mathematical language seems to need >6 components
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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).
>>>>>>>>>>>>>
>>>>>>>>>>>>> This is starting to show up in the hardware area (e.g.
>>>>>>>>>>>>> Lamport's TLC[0])
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 2) We need "scaffolding". That is, we need a theory
>>>>>>>>>>>>> that can be reduced to some implementable form
>>>>>>>>>>>>> that provides concept-level structure.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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)
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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 ...
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I am looking at LEAN's definitions and theorems with
>>>>>>>>>>>>> an eye to "spreading" them into the group scaffold of
>>>>>>>>>>>>> Axiom.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 4) We need "carriers" (Axiom calls them representations,
>>>>>>>>>>>>> aka "REP"). REPs allow data structures to be defined
>>>>>>>>>>>>> independent of the implementation.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Axiom "got this wrong" because it didn't sufficiently
>>>>>>>>>>>>> separate the REP from the "Domain". I plan to fix this.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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:
>>>>>>>>>>>>>
>>>>>>>>>>>>>   A) has an argument list of "Categories" that this "Domain"
>>>>>>>>>>>>>       box inherits. Thus, the "Integer Domain" inherits
>>>>>>>>>>>>>       the definitions and axioms from "Commutative"
>>>>>>>>>>>>>
>>>>>>>>>>>>>      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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>   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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>       Functions in the Domain box can use all of
>>>>>>>>>>>>>       the definitions and axioms about the representation
>>>>>>>>>>>>>       (e.g. NonNegativeIntegers are always positive)
>>>>>>>>>>>>>
>>>>>>>>>>>>>   C) contains local "spread" definitions and axioms
>>>>>>>>>>>>>        that can be used in function proofs.
>>>>>>>>>>>>>
>>>>>>>>>>>>>       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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>   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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>   E) contains implementations of inherited functions.
>>>>>>>>>>>>>
>>>>>>>>>>>>>        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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>       Axiom has about 20 GCD implementations that
>>>>>>>>>>>>>       differ locally from the default in the category. They
>>>>>>>>>>>>>       use properties known locally to be more efficient.
>>>>>>>>>>>>>
>>>>>>>>>>>>>   F) contains local function signatures.
>>>>>>>>>>>>>
>>>>>>>>>>>>>       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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>       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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>       In addition, local "helper" functions need their
>>>>>>>>>>>>>       own signatures that are not user visible.
>>>>>>>>>>>>>
>>>>>>>>>>>>>   G) the function implementation for each signature.
>>>>>>>>>>>>>
>>>>>>>>>>>>>        This is obviously where all the magic happens
>>>>>>>>>>>>>
>>>>>>>>>>>>>   H) the proof of each function.
>>>>>>>>>>>>>
>>>>>>>>>>>>>        This is where I'm using LEAN.
>>>>>>>>>>>>>
>>>>>>>>>>>>>        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.
>>>>>>>>>>>>>
>>>>>>>>>>>>>    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 :-)
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 6) User level presentation.
>>>>>>>>>>>>>
>>>>>>>>>>>>>     This is where the systems can differ significantly.
>>>>>>>>>>>>>     Axiom and LEAN both have GCD but they use
>>>>>>>>>>>>>     that for different purposes.
>>>>>>>>>>>>>
>>>>>>>>>>>>>     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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 7) Trust
>>>>>>>>>>>>>
>>>>>>>>>>>>> Unlike everything else, computational mathematics
>>>>>>>>>>>>> can have proven code that gives various guarantees.
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> (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).
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Tim
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> [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)
>>>>>>>>>>>>>
>>>>>>>>>>>>> [1] https://www.tul.com.tw/productspynq-z2.html
>>>>>>>>>>>>>
>>>>>>>>>>>>> [2] https://www.youtube.com/watch?v=3DdCuZkaaou0Q
>>>>>>>>>>>>>
>>>>>>>>>>>>> [3] "ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE"
>>>>>>>>>>>>> https://arxiv.org/pdf/1307.3091.pdf
>>>>>>>>>>>>>
>>>>>>>>>>>>> [4] ALICE Chatbot
>>>>>>>>>>>>>
>>>>>>>>>>>>> http://www.scielo.org.mx/pdf/cys/v19n4/1405-5546-cys-19-04-00=
625.pdf
>>>>>>>>>>>>>
>>>>>>>>>>>>> [5] OPS5 User Manual
>>>>>>>>>>>>>
>>>>>>>>>>>>> https://kilthub.cmu.edu/articles/journal_contribution/OPS5_us=
er_s_manual/6608090/1
>>>>>>>>>>>>>
>>>>>>>>>>>>> [6] Scott Fahlman "SCONE"
>>>>>>>>>>>>> http://www.cs.cmu.edu/~sef/scone/
>>>>>>>>>>>>>
>>>>>>>>>>>>> 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 w=
ho
>>>>>>>>>>>>> > 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" amon=
g
>>>>>>>>>>>>> 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-processin=
g-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-scie=
ntific-software.html
>>>>>>>>>>>>> >>
>>>>>>>>>>>>> >> which is a really interesting read. For example"
>>>>>>>>>>>>> >>
>>>>>>>>>>>>> >>  [Hatton1994], is now a quarter of a century old, but its
>>>>>>>>>>>>> conclusions
>>>>>>>>>>>>> >> are still fresh. The authors fed the 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 catego=
ry
>>>>>>>>>>>>> >>>> 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 th=
e
>>>>>>>>>>>>> >>>> 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-you-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. Th=
e
>>>>>>>>>>>>> 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 wha=
t
>>>>>>>>>>>>> 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 that
>>>>>>>>>>>>> >>>>>> calculus (a model not
>>>>>>>>>>>>> >>>>>>    unlike a meta-circular interpreter, but connected t=
o
>>>>>>>>>>>>> the
>>>>>>>>>>>>> >>>>>> fundamental operations of the
>>>>>>>>>>>>> >>>>>>    machine in such a way as to provide, at any point i=
n
>>>>>>>>>>>>> a
>>>>>>>>>>>>> >>>>>> computation,
>>>>>>>>>>>>> >>>>>> fully articulated
>>>>>>>>>>>>> >>>>>>    descriptions of the state of that computation, for
>>>>>>>>>>>>> inspection and
>>>>>>>>>>>>> >>>>>> possible modification). In
>>>>>>>>>>>>> >>>>>>    terms of the theories that result from these
>>>>>>>>>>>>> investigations, we
>>>>>>>>>>>>> >>>>>> present a general architecture
>>>>>>>>>>>>> >>>>>>    for procedurally reflective processes, able to shif=
t
>>>>>>>>>>>>> smoothly
>>>>>>>>>>>>> >>>>>> between dealing with a given
>>>>>>>>>>>>> >>>>>>    subject domain, and dealing with their own reasonin=
g
>>>>>>>>>>>>> processes
>>>>>>>>>>>>> >>>>>> over
>>>>>>>>>>>>> >>>>>> that domain.
>>>>>>>>>>>>> >>>>>>
>>>>>>>>>>>>> >>>>>>    An instance of the general solution is worked out i=
n
>>>>>>>>>>>>> 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 which
>>>>>>>>>>>>> >>>>>> the respective categories
>>>>>>>>>>>>> >>>>>>    of notation, structure, semantics, and behaviour ar=
e
>>>>>>>>>>>>> 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 towe=
r
>>>>>>>>>>>>> of proofs at
>>>>>>>>>>>>> >>>>>> 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 build
>>>>>>>>>>>>> >>>>>> "all the way down to the
>>>>>>>>>>>>> >>>>>> metal". If each layer is constructed on top of previou=
s
>>>>>>>>>>>>> proven layers
>>>>>>>>>>>>> >>>>>> 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 i=
n
>>>>>>>>>>>>> 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 adap=
t
>>>>>>>>>>>>> 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 paralle=
l
>>>>>>>>>>>>> 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 o=
f
>>>>>>>>>>>>> "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, an=
d
>>>>>>>>>>>>> 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 ther=
e
>>>>>>>>>>>>> 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 i=
t
>>>>>>>>>>>>> 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 it=
s
>>>>>>>>>>>>> own core.
>>>>>>>>>>>>> >>>>>>>
>>>>>>>>>>>>> >>>>>>> In addition. notice that each domain is independent o=
f
>>>>>>>>>>>>> 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. Se=
e
>>>>>>>>>>>>> >>>>>>>> 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 an=
d
>>>>>>>>>>>>> expect to
>>>>>>>>>>>>> >>>>>>>>> work directly in files and multiple buffers. When I
>>>>>>>>>>>>> try to use one
>>>>>>>>>>>>> >>>>>>>>> of the many IDE tools I find they tend to "get in
>>>>>>>>>>>>> the way". I
>>>>>>>>>>>>> >>>>>>>>> already
>>>>>>>>>>>>> >>>>>>>>> know or can quickly find whatever they try to tell
>>>>>>>>>>>>> me. If you use
>>>>>>>>>>>>> >>>>>>>>> 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 actuall=
y
>>>>>>>>>>>>> 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. Thi=
s
>>>>>>>>>>>>> loop catches
>>>>>>>>>>>>> >>>>>>>>> errors in both the latex and the source code.
>>>>>>>>>>>>> Keeping an open file
>>>>>>>>>>>>> >>>>>>>>> in
>>>>>>>>>>>>> >>>>>>>>> my pdf viewer shows all of the changes in the
>>>>>>>>>>>>> document after every
>>>>>>>>>>>>> >>>>>>>>> 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 is
>>>>>>>>>>>>> >>>>>>>>> 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 advanc=
e
>>>>>>>>>>>>> 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, shapin=
g
>>>>>>>>>>>>> it to your
>>>>>>>>>>>>> >>>>>>>>>> need.
>>>>>>>>>>>>> >>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>> My current thread of study is software
>>>>>>>>>>>>> architecture. See
>>>>>>>>>>>>> >>>>>>>>>>
>>>>>>>>>>>>> https://www.youtube.com/watch?v=3DW2hagw1VhhI&feature=3Dyoutu=
.be
>>>>>>>>>>>>> >>>>>>>>>> and https://www.georgefairbanks.com/videos/
>>>>>>>>>>>>> >>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>> My current thinking on SANE involves the ability t=
o
>>>>>>>>>>>>> >>>>>>>>>> dynamically define categories, representations, an=
d
>>>>>>>>>>>>> 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 careful
>>>>>>>>>>>>> >>>>>>>>>> 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 type
>>>>>>>>>>>>> >>>>>>>>>>> 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 to
>>>>>>>>>>>>> >>>>>>>>>>> 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 both
>>>>>>>>>>>>> >>>>>>>>>>> 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 have
>>>>>>>>>>>>> >>>>>>>>>>> + 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 an
>>>>>>>>>>>>> >>>>>>>>>>> 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 of
>>>>>>>>>>>>> >>>>>>>>>>>> the
>>>>>>>>>>>>> >>>>>>>>>>>> ideas.
>>>>>>>>>>>>> >>>>>>>>>>>> In particular, source code gets compiled into
>>>>>>>>>>>>> data structures.
>>>>>>>>>>>>> >>>>>>>>>>>> In
>>>>>>>>>>>>> >>>>>>>>>>>> Axiom
>>>>>>>>>>>>> >>>>>>>>>>>> these data structures really are a graph of
>>>>>>>>>>>>> related structures.
>>>>>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>>> For example, looking at the gcd function from
>>>>>>>>>>>>> NNI, there is the
>>>>>>>>>>>>> >>>>>>>>>>>> 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 from
>>>>>>>>>>>>> >>>>>>>>>>>> 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 useful
>>>>>>>>>>>>> >>>>>>>>>>>> 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 be
>>>>>>>>>>>>> >>>>>>>>>>>> "in
>>>>>>>>>>>>> >>>>>>>>>>>> a
>>>>>>>>>>>>> >>>>>>>>>>>> single tab to show the graph" or "the nodes of
>>>>>>>>>>>>> the graph are in
>>>>>>>>>>>>> >>>>>>>>>>>> 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 shoul=
d
>>>>>>>>>>>>> be possible
>>>>>>>>>>>>> >>>>>>>>>>>> to
>>>>>>>>>>>>> >>>>>>>>>>>> look
>>>>>>>>>>>>> >>>>>>>>>>>> at
>>>>>>>>>>>>> >>>>>>>>>>>> the code in its literate form with the
>>>>>>>>>>>>> surrounding explanation.
>>>>>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>>> 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, they
>>>>>>>>>>>>> >>>>>>>>>>>> have
>>>>>>>>>>>>> >>>>>>>>>>>> access to display (and modify) the Axiom
>>>>>>>>>>>>> workspace at all
>>>>>>>>>>>>> >>>>>>>>>>>> times.
>>>>>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>>> The only hesitation is that McClim uses quicklis=
p
>>>>>>>>>>>>> and drags in
>>>>>>>>>>>>> >>>>>>>>>>>> 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 mis=
s.
>>>>>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>>> 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 ha=
s
>>>>>>>>>>>>> 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 mu=
ch
>>>>>>>>>>>>> >>>>>>>>>>>>>> documentation to create, how to pass along tac=
it
>>>>>>>>>>>>> >>>>>>>>>>>>>> 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 an=
d
>>>>>>>>>>>>> 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 also
>>>>>>>>>>>>> >>>>>>>>>>>>>> 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
>>>>>>>>>>>>> >>>>>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>>
>>>>>>>>>>>>> >>>>>>>>
>>>>>>>>>>>>> >>>>>>>
>>>>>>>>>>>>> >>>>>>
>>>>>>>>>>>>> >>>>>
>>>>>>>>>>>>> >>>>
>>>>>>>>>>>>> >>>
>>>>>>>>>>>>> >>
>>>>>>>>>>>>> >
>>>>>>>>>>>>>
>>>>>>>>>>>>

--000000000000cf249d05da14f883
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Axiom has an awkward &#39;attributes&#39; category st=
ructure.</div><div><br></div><div>In the SANE version it is clear that thes=
e attributes are much</div><div>closer to logic &#39;definitions&#39;. As a=
 result one of the changes</div><div>is to create a new &#39;category&#39;-=
type structure for definitions.</div><div>There will be a new keyword, like=
 the category keyword,</div><div>&#39;definition&#39;.</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 Fri, Mar 11, 2022 at 9:46 AM Tim Daly &lt;=
<a href=3D"mailto:[email protected]">[email protected]</a>&gt; wrote:<br>=
</div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;b=
order-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"ltr"><d=
iv>The github lockout continues... <br></div><div><br></div><div>I&#39;m sp=
ending some time adding examples to source code.</div><div><br></div><div>A=
ny function can have ++X comments added. These will</div><div>appear as exa=
mples when the function is )display For example,</div><div>in PermutationGr=
oup there is a function &#39;strongGenerators&#39;</div><div>defined as:</d=
iv><div><br></div><div>=C2=A0 strongGenerators : % -&gt; L PERM S</div><div=
>=C2=A0=C2=A0=C2=A0 ++ strongGenerators(gp) returns strong generators for</=
div><div>=C2=A0=C2=A0=C2=A0 ++ the group gp.</div><div>=C2=A0=C2=A0=C2=A0 +=
+</div><div>=C2=A0=C2=A0=C2=A0 ++X S:List(Integer) :=3D [1,2,3,4]</div><div=
>=C2=A0=C2=A0=C2=A0 ++X G :=3D symmetricGroup(S)</div><div>=C2=A0=C2=A0=C2=
=A0 ++X strongGenerators(G)</div><div><br></div><div><br></div><div><br></d=
iv><div>Later, in the interpreter we see:</div><div><br></div><div><br></di=
v><div><br></div><div><br></div><div>)d op strongGenerators</div><div><br><=
/div><div>=C2=A0 There is one exposed function called strongGenerators :</d=
iv><div>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 [1] PermutationGroup(D2) -&gt; List(=
Permutation(D2)) from</div><div>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 PermutationGroup(D2)</div><div>=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0 if D2 has SETCAT</div><div><br></div><div>=C2=A0 Exam=
ples of strongGenerators from PermutationGroup</div><div>=C2=A0 <br></div><=
div>=C2=A0 S:List(Integer) :=3D [1,2,3,4]</div><div>=C2=A0 G :=3D symmetric=
Group(S)</div><div>=C2=A0 strongGenerators(G)</div><div><br></div><div><br>=
</div><div><br></div><div><br></div><div>This will show a working example f=
or functions that the</div><div>user can copy and use. It is especially use=
ful to show how</div><div>to construct working arguments.</div><div><br></d=
iv><div>These &quot;example&quot; functions are run at build time when</div=
><div>the make command looks like</div><div>=C2=A0=C2=A0=C2=A0 make TESTSET=
=3Dalltests<br></div><div><br></div><div>I hope to add this documentation t=
o all Axiom functions.</div><div><br></div><div>In addition, the plan is to=
 add these function calls to the</div><div>usual test documentation. That m=
eans 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 expected output.<br></div><div><br></di=
v><div>Tim</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 Fri, Feb 25=
, 2022 at 6:05 PM 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(2=
04,204,204);padding-left:1ex"><div dir=3D"ltr"><div>It turns out that creat=
ing SPAD-looking output is trivial <br></div><div>in Common Lisp. Each clas=
s can have a custom print</div><div>routine so signatures and ++ comments c=
an each be</div><div>printed with their own format.</div><div><br></div><di=
v>To ensure that I maintain compatibility I&#39;ll be printing</div><div>th=
e categories and domains so they look like SPAD code,</div><div>at least un=
til I get the proof technology integrated. I will</div><div>probably specia=
lize the proof printers to look like the</div><div>original LEAN proof synt=
ax.</div><div><br></div><div>Internally, however, it will all be Common Lis=
p.</div><div><br></div><div>Common Lisp makes so many desirable features so=
 easy.</div><div>It is possible to trace dynamically at any level. One coul=
d</div><div>even write a trace that showed how Axiom arrived at the</div><d=
iv>solution. Any domain could have special case output syntax</div><div>wit=
hout affecting any other domain so one could write a</div><div>tree-like ou=
tput for proofs. Using greek characters is trivial</div><div>so the input a=
nd output notation is more mathematical.<br></div><div><br></div><div>Tim</=
div><div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D"ltr" cl=
ass=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; wr=
ote:<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>Axiom&#39;s SPAD code compiles to Common Lisp.</div><div>The AKC=
L version of Common Lisp compiles to C.</div><div>Three languages and 2 com=
pilers is a lot to maintain.</div><div>Further, there are very few people a=
ble to write SPAD</div><div>and even fewer people able to maintain it.<br><=
/div><div><br></div><div>I&#39;ve decided that the SANE version of Axiom wi=
ll be <br></div><div>implemented in pure Common Lisp. I&#39;ve outlined Axi=
om&#39;s<br></div><div>category / type hierarchy in the Common Lisp Object<=
/div><div>System (CLOS). I am now experimenting with re-writing</div><div>t=
he functions into Common Lisp.<br></div><div><br></div><div>This will have =
several long-term effects. It simplifies</div><div>the implementation issue=
s. SPAD code blocks a lot of</div><div>actions and optimizations that Commo=
n Lisp provides.</div><div>The Common Lisp language has many more people<br=
></div><div>who can read, modify, and maintain code. It provides for</div><=
div>interoperability with other Common Lisp projects with</div><div>no effo=
rt. Common Lisp is an international standard</div><div>which ensures that t=
he code will continue to run.<br></div><div><br></div><div>The input / outp=
ut mathematics will remain the same.</div><div>Indeed, with the new general=
izations for first-class</div><div>dependent types it will be more general.=
</div><div><br></div><div>This is a big change, similar to eliminating BOOT=
 code</div><div>and moving to Literate Programming. This will provide a</di=
v><div>better platform for future research work. Current research</div><div=
>is focused on merging Axiom&#39;s computer algebra mathematics</div><div>w=
ith Lean&#39;s proof language. The goal is to create a system for</div><div=
>=C2=A0&quot;computational mathematics&quot;.<br></div><div><br></div><div>=
Research is the whole point of Axiom.</div><div><br></div><div>Tim</div><di=
v><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 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>I can&#39;t stress enough how important it is to listen t=
o Hamming&#39;s talk</div><div><a href=3D"https://www.youtube.com/watch?v=
=3Da1zDuOPkMSw" target=3D"_blank">https://www.youtube.com/watch?v=3Da1zDuOP=
kMSw</a></div><div><br></div><div>Axiom will begin to die the day I stop wo=
rking on it.</div><div><br></div><div>However, proving Axiom correct &quot;=
down to the metal&quot;, is fundamental.</div><div>It will merge computer a=
lgebra and logic, spawning years of new</div><div>research.</div><div><br><=
/div><div>Work on fundamental 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, Dec 30, 2021 at 6:46 PM Tim Daly &lt;<a href=3D"mai=
lto:[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:=
<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8=
ex;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>i=
s &quot;what functions were called and what was their return value?&quot;</=
div><div>Otherwise known as the &quot;show your work&quot; idea.</div><div>=
<br></div><div>There is an idea called the &quot;writer monad&quot; [0], us=
ually <br></div><div>implemented to facilitate logging. We can exploit this=
</div><div>idea to provide &quot;show your work&quot; capability. Each func=
tion</div><div>can provide this information inside the monad enabling the</=
div><div>question to be answered at any time.</div><div><br></div><div>For =
those unfamiliar with the monad idea, the best explanation</div><div>I&#39;=
ve found is this video [1].</div><div><br></div><div>Tim<br></div><div><br>=
</div><div>[0] Deriving the writer monad from first principles<br></div><di=
v><a href=3D"https://williamyaoh.com/posts/2020-07-26-deriving-writer-monad=
.html" target=3D"_blank">https://williamyaoh.com/posts/2020-07-26-deriving-=
writer-monad.html</a></div><div><br></div><div>[1] The Absolute Best Intro =
to Monads for Software Engineers</div><div><a href=3D"https://www.youtube.c=
om/watch?v=3DC2w45qRc3aU" target=3D"_blank">https://www.youtube.com/watch?v=
=3DC2w45qRc3aU</a></div></div><br><div class=3D"gmail_quote"><div dir=3D"lt=
r" class=3D"gmail_attr">On Mon, Dec 13, 2021 at 12:30 AM Tim Daly &lt;<a hr=
ef=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>&g=
t; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0p=
x 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div d=
ir=3D"ltr"><div>...(snip)...<br></div><div><br></div><div>Common Lisp has a=
n &quot;open compiler&quot;. That allows the ability</div><div>to deeply mo=
dify compiler behavior using compiler macros</div><div>and macros in genera=
l. CLOS takes advantage of this to add</div><div>typed behavior into the co=
mpiler in a way that ALLOWS strict</div><div>typing such as found in constr=
uctive type theory and ML.</div><div>Judgments, ala Crary, are front-and-ce=
nter.<br></div><div><br></div><div>Whether you USE the discipline afforded =
is the real question.</div><div><br></div><div>Indeed, the Axiom research s=
truggle is essentially one of how</div><div>to have a disciplined use of fi=
rst-class dependent types. The</div><div>struggle raises issues of, for exa=
mple, compiling a dependent</div><div>type whose argument is recursive in t=
he compiled type. Since</div><div>the new type is first-class it can be con=
structed at what you</div><div>improperly call &quot;run-time&quot;. Howeve=
r, it appears that the recursive</div><div>type may have to call the compil=
er at each recursion to generate</div><div>the next step since in some case=
s it cannot generate &quot;closed code&quot;.<br></div><div><br></div><div>=
I am embedding proofs (in LEAN language) into the type</div><div>hierarchy =
so that theorems, which depend on the type hierarchy,<br></div><div>are cor=
rectly inherited. The compiler has to check the proofs of functions</div><d=
iv>at compile time using these. Hacking up nonsense just won&#39;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=
 is a</div><div>field (cough)). The type inherits this theorem and proofs o=
f</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</di=
v><div>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 yet, LEAN is a moving target. Sigh.)<br></div><div><br><br></div></d=
iv><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On =
Thu, Nov 25, 2021 at 9:43 AM Tim Daly &lt;<a href=3D"mailto:axiomcas@gmail.=
com" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blockquo=
te 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&#39;ve been re-architect=
ing Axiom to use first class</div><div>dependent types and proving the algo=
rithms correct. For example,</div><div>the GCD of natural numbers or the GC=
D of polynomials.</div><div><br></div><div>The idea involves &quot;boxing u=
p&quot; the proof with the algorithm (aka</div><div>proof carrying code) in=
 the ELF file (under a crypto hash so it</div><div>can&#39;t be changed).</=
div><div><br></div><div>Once the code is running on the CPU, the proof is r=
un in parallel</div><div>on the field programmable gate array (FPGA). Intel=
 data center</div><div>servers have CPUs with built-in FPGAs these days.</d=
iv><div><br></div><div>There is a bit of a disconnect, though. The 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 compiled the=
 GCD</div><div>code to machine code, it also compiled the proof to &quot;ma=
chine code&quot;.</div><div>That is, for each machine instruction, the FPGA=
 proof checker</div><div>would ensure that the proof was not violated at th=
e individual</div><div>instruction level.<br></div><div><br></div><div>What=
 does it mean to &quot;compile a proof to the machine code level&quot;?</di=
v><div><br></div><div>The Milawa effort (Myre14.pdf) does incremental proof=
s in layers.</div><div>To quote from the article [0]:<br></div><div><br></d=
iv><div>=C2=A0=C2=A0 We begin with a simple proof checker, call it A, which=
 is short</div><div>=C2=A0=C2=A0 enough to verify by the ``social process&#=
39;&#39; of mathematics -- and</div><div>=C2=A0 more recently with a theore=
m prover for a more expressive logic.</div><div><br></div><div>=C2=A0=C2=A0=
 We then develop a series of increasingly powerful proof checkers,</div><di=
v>=C2=A0 call the B, C, D, and so on. We show each of these programs only</=
div><div>=C2=A0=C2=A0 accepts the same formulas as A, using A to verify B, =
and B to verify</div><div>=C2=A0=C2=A0 C, and so on. Then, since we trust A=
, and A says B is trustworthy, we</div><div>=C2=A0=C2=A0 can trust B. Then,=
 since we trust B, and B says C is trustworthy, we</div><div>=C2=A0=C2=A0 c=
an trust C. <br></div><div><br></div><div>This gives a technique for &quot;=
compiling the proof&quot; down the the machine</div><div>code level. Ideall=
y, the compiler would have judgments for each step of</div><div>the compila=
tion so that each compile step has a justification. I don&#39;t</div><div>k=
now of any compiler that does this yet. (References welcome).<br></div><div=
><div><br></div><div>At the machine code level, there are techniques that w=
ould allow</div><div>the FPGA proof to &quot;step in sequence&quot; with th=
e executing code.<br></div><div>Some work has been done on using &quot;Hoar=
e Logic for Realistically</div><div>Modelled Machine Code&quot; (paper atta=
ched, Myre07a.pdf),</div><div>&quot;Decompilation into Logic -- Improved (M=
yre12a.pdf).</div><div><br></div><div>So the game is to construct a GCD ove=
r some type (Nats, Polys, etc.</div><div>Axiom has 22), compile the depende=
nt type GCD to machine code.</div><div>In parallel, the proof of the code i=
s compiled to machine code. The</div><div>pair is sent to the CPU/FPGA and,=
 while the algorithm runs, the FPGA</div><div>ensures the proof is not viol=
ated, instruction by instruction.</div><div><br></div><div>(I&#39;m ignorin=
g machine architecture issues such pipelining, out-of-order,</div><div>bran=
ch prediction, and other machine-level things to ponder. I&#39;m looking</d=
iv><div>at the RISC-V Verilog details by various people to understand bette=
r but</div><div>it is still a &quot;misty fog&quot; for me.)<br></div><div>=
<br></div><div>The result is proven code &quot;down to the metal&quot;.</di=
v><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/moore/acl2/manuals/cur=
rent/manual/index-seo.php/ACL2____MILAWA" target=3D"_blank">https://www.cs.=
utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____MI=
LAWA</a></div></div></div></div></div><br><div class=3D"gmail_quote"><div d=
ir=3D"ltr" class=3D"gmail_attr">On Thu, Nov 25, 2021 at 6:05 AM Tim Daly &l=
t;<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]=
m</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"><br><div dir=3D"ltr"><div>As you know I&#39;ve been re-ar=
chitecting Axiom to use first class</div><div>dependent types and proving t=
he algorithms correct. For example,</div><div>the GCD of natural numbers or=
 the GCD of polynomials.</div><div><br></div><div>The idea involves &quot;b=
oxing up&quot; the proof with the algorithm (aka</div><div>proof carrying c=
ode) in the ELF file (under a crypto hash so it</div><div>can&#39;t be chan=
ged).</div><div><br></div><div>Once the code is running on the CPU, the pro=
of 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 these d=
ays.</div><div><br></div><div>There is a bit of a disconnect, though. The G=
CD code is compiled</div><div>machine code but the proof is LEAN-level.</di=
v><div><br></div><div>What would be ideal is if the compiler not only compi=
led the GCD</div><div>code to machine code, it also compiled the proof to &=
quot;machine code&quot;.</div><div>That is, for each machine instruction, t=
he FPGA proof checker</div><div>would ensure that the proof was not violate=
d at the individual</div><div>instruction level.<br></div><div><br></div><d=
iv>What does it mean to &quot;compile a proof to the machine code level&quo=
t;?</div><div><br></div><div>The Milawa effort (Myre14.pdf) does incrementa=
l proofs in layers.</div><div>To quote from the article [0]:<br></div><div>=
<br></div><div>=C2=A0=C2=A0 We begin with a simple proof checker, call it A=
, which is short</div><div>=C2=A0=C2=A0 enough to verify by the ``social pr=
ocess&#39;&#39; of mathematics -- and</div><div>=C2=A0 more recently with a=
 theorem prover for a more expressive logic.</div><div><br></div><div>=C2=
=A0=C2=A0 We then develop a series of increasingly powerful proof checkers,=
</div><div>=C2=A0 call the B, C, D, and so on. We show each of these progra=
ms only</div><div>=C2=A0=C2=A0 accepts the same formulas as A, using A to v=
erify B, and B to verify</div><div>=C2=A0=C2=A0 C, and so on. Then, since w=
e trust A, and A says B is trustworthy, we</div><div>=C2=A0=C2=A0 can trust=
 B. Then, since we trust B, and B says C is trustworthy, we</div><div>=C2=
=A0=C2=A0 can trust C. <br></div><div><br></div><div>This gives a technique=
 for &quot;compiling the proof&quot; down the the machine</div><div>code le=
vel. Ideally, the compiler would have judgments for each step of</div><div>=
the compilation so that each compile step has a justification. I don&#39;t<=
/div><div>know of any compiler that does this yet. (References welcome).<br=
></div><div><div><br></div><div>At the machine code level, there are techni=
ques that would allow</div><div>the FPGA proof to &quot;step in sequence&qu=
ot; with the executing code.<br></div><div>Some work has been done on using=
 &quot;Hoare Logic for Realistically</div><div>Modelled Machine Code&quot; =
(paper attached, Myre07a.pdf),</div><div>&quot;Decompilation into Logic -- =
Improved (Myre12a.pdf).</div><div><br></div><div>So the game is to construc=
t a GCD over some type (Nats, Polys, etc.</div><div>Axiom has 22), compile =
the dependent type GCD to machine code.</div><div>In parallel, the proof of=
 the code is compiled to machine code. The</div><div>pair is sent to the CP=
U/FPGA and, while the algorithm runs, the FPGA</div><div>ensures the proof =
is not violated, instruction by instruction.</div><div><br></div><div>(I&#3=
9;m ignoring machine architecture issues such pipelining, out-of-order,</di=
v><div>branch prediction, and other machine-level things to ponder. I&#39;m=
 looking</div><div>at the RISC-V Verilog details by various people to under=
stand better but</div><div>it is still a &quot;misty fog&quot; for me.)<br>=
</div><div><br></div><div>The result is proven code &quot;down to the metal=
&quot;.</div><div><br></div><div>Tim</div><div><br></div><div><br></div><di=
v><br></div><div>[0] <a href=3D"https://www.cs.utexas.edu/users/moore/acl2/=
manuals/current/manual/index-seo.php/ACL2____MILAWA" target=3D"_blank">http=
s://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_quote"><=
div dir=3D"ltr" class=3D"gmail_attr">On Sat, Nov 13, 2021 at 5:28 PM Tim Da=
ly &lt;<a href=3D"mailto:[email protected]" target=3D"_blank">axiomcas@gma=
il.com</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"m=
argin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left=
: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 so=
me language</div><div>design questions.</div><div><br></div><div>Given that=
 mathematics is such a general subject with a lot of</div><div>&quot;local&=
quot; notation and ideas (witness logical judgment notation)</div><div>care=
ful 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-l=
evel process. The language</div><div>designer creates a language and then a=
n implementation. Various</div><div>design choices affect the final languag=
e.<br></div><div><br></div><div>There is &quot;The Metaobject Protocol&quot=
; (MOP)<br></div><div><a href=3D"https://www.amazon.com/Art-Metaobject-Prot=
ocol-Gregor-Kiczales/dp/0262610744" target=3D"_blank">https://www.amazon.co=
m/Art-Metaobject-Protocol-Gregor-Kiczales/dp/0262610744</a></div><div>which=
 encourages a three-level process. The language designer <br></div><div>wor=
ks at a Metalevel to design a family of languages, then the</div><div>langu=
age specializations, then the implementation. A MOP design</div><div>allows=
 the language user to optimize the language to their problem.</div><div><br=
></div><div>A simple paper on the subject is &quot;Metaobject Protocols&quo=
t;</div><div><a href=3D"https://users.cs.duke.edu/~vahdat/ps/mop.pdf" targe=
t=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"><d=
iv dir=3D"ltr" class=3D"gmail_attr">On Mon, Oct 25, 2021 at 7:42 PM Tim Dal=
y &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"ma=
rgin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:=
1ex"><div dir=3D"ltr"><div>I have a separate thread of research on Self-Rep=
licating Systems</div><div>(ref: Kinematics of Self Reproducing Machines</d=
iv><div><a href=3D"http://www.molecularassembler.com/KSRM.htm" target=3D"_b=
lank">http://www.molecularassembler.com/KSRM.htm</a>)<br></div><div><br></d=
iv><div>which led to watching &quot;Strange Dreams of Stranger Loops&quot; =
by Will Byrd</div><div><a href=3D"https://www.youtube.com/watch?v=3DAffW-7i=
ka0E" 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><div=
>&quot;A Model for Deliberation, Action, and Introspection&quot;</div><div>=
<br></div><div>I also read the thesis by J.C.G. Sturdy</div><div>&quot;A Li=
sp through the Looking Glass&quot;</div><div><br></div><div>Self-replicatio=
n requires the ability to manipulate your own</div><div>representation in s=
uch a way that changes to that representation</div><div>will change behavio=
r.</div><div><br></div><div>This leads to two thoughts in the SANE research=
.</div><div><br></div><div>First, &quot;Declarative Representation&quot;. T=
hat is, most of the things</div><div>about the representation should be dec=
larative rather than</div><div>procedural. Applying this idea as much as po=
ssible makes it</div><div>easier to understand and manipulate.<br></div><di=
v><br></div><div>Second, &quot;Explicit Call Stack&quot;. Function calls fo=
rm an implicit</div><div>call stack. This can usually be displayed in a run=
ning lisp system.</div><div>However, having the call stack explicitly avail=
able would mean</div><div>that a system could &quot;introspect&quot; 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 &quot;show the work&quot;. O=
ne of the normal complaints is that</div><div>a system presents an answer b=
ut there is no way to know how</div><div>that answer was derived. These two=
 ideas make it possible to</div><div>understand, display, and even post-ans=
wer manipulate</div><div>the intermediate steps.</div><div><br></div><div>H=
aving the 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 parallel 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 h=
ref=3D"mailto:[email protected]" target=3D"_blank">[email protected]</a>&=
gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0=
px 0px 0.8ex;border-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></div><div>The categories and domains constructed using categ=
ories</div><div>are dependent types. When are dependent types &quot;equal&q=
uot;?</div><div>Well, hummmm, that depends on the arguments to the</div><di=
v>constructor.</div><div><br></div><div>But in order to decide(?) equality =
we have to evaluate</div><div>the arguments (which themselves can be depend=
ent types).</div><div>Indeed, we may, and in general, we must evaluate the =
<br></div><div>arguments at compile time (well, &quot;construction time&quo=
t; as</div><div>there isn&#39;t really a compiler / interpreter separation =
anymore.)<br></div><div><br></div><div>That raises the question of what &qu=
ot;equality&quot; means. This</div><div>is not simply a &quot;set equality&=
quot; relation. It falls into the</div><div>infinite-groupoid of homotopy t=
ype theory. In general</div><div>it appears that deciding category / domain=
 equivalence</div><div>might force us to climb the type hierarchy.</div><di=
v><br></div><div>Beyond that, there is the question of &quot;which proof&qu=
ot;</div><div>applies to the resulting object. Proofs depend on their</div>=
<div>assumptions which might be different for different</div><div>construct=
ions. As yet I have no clue how to &quot;index&quot;</div><div>proofs based=
 on their assumptions, nor how to <br></div><div>connect these assumptions =
to the groupoid structure.</div><div><br></div><div>My brain hurts.</div><d=
iv><br></div><div>Tim</div><div><br></div></div><br><div class=3D"gmail_quo=
te"><div dir=3D"ltr" class=3D"gmail_attr">On Mon, Oct 18, 2021 at 2:00 AM T=
im Daly &lt;<a href=3D"mailto:[email protected]" target=3D"_blank">axiomca=
[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>&quot;Birthing Computational Mathematics&q=
uot;</div><div><br></div><div>The Axiom SANE project is difficult at a very=
 fundamental</div><div>level. The title &quot;SANE&quot; was chosen due to =
the various</div><div>words found in a thesuarus... &quot;rational&quot;, &=
quot;coherent&quot;,</div><div>&quot;judicious&quot; and &quot;sound&quot;.=
</div><div><br></div><div>These are very high level, amorphous ideas. But s=
o is</div><div>the design of SANE. Breaking away from tradition in</div><di=
v>computer algebra, type theory, and proof assistants</div><div>is very dif=
ficult. Ideas tend to fall into standard jargon</div><div>which limits both=
 the frame of thinking (e.g. dependent</div><div>types) and the content (e.=
g. notation).</div><div><br></div><div>Questioning both frame and content i=
s very difficult.</div><div>It is hard to even recognize when they are acce=
pted</div><div>&quot;by default&quot; rather than &quot;by choice&quot;. Wh=
at does the idea<br></div><div>&quot;power tools&quot; mean in a primitive,=
 hand labor culture?<br></div><div><br></div><div>Christopher Alexander [0]=
 addresses this problem in</div><div>a lot of his writing. Specifically, in=
 his book &quot;Notes on</div><div>the Synthesis of Form&quot;, in his chap=
ter 5 &quot;The Selfconsious</div><div>Process&quot;, he addresses this pro=
blem directly. This is a</div><div>&quot;must read&quot; book.<br></div><di=
v><br></div><div>Unlike building design and contruction, however, there</di=
v><div>are almost no constraints to use as guides. Alexander</div><div>quot=
es Plato&#39;s Phaedrus:</div><div><br></div><div>=C2=A0 &quot;First, the t=
aking in of scattered particulars under</div><div>=C2=A0=C2=A0 one Idea, so=
 that everyone understands what is being</div><div>=C2=A0=C2=A0 talked abou=
t ... Second, the separation of the Idea</div><div>=C2=A0=C2=A0 into parts,=
 by dividing it at the joints, as nature</div><div>=C2=A0=C2=A0 directs, no=
t breaking any limb in half as a bad <br></div><div>=C2=A0=C2=A0 carver mig=
ht.&quot;<br></div><div><br></div><div>Lisp, which has been called &quot;cl=
ay for the mind&quot; can</div><div>build virtually anything that can be th=
ought. The <br></div><div>&quot;joints&quot; are also &quot;of one&#39;s ch=
oosing&quot; so one is</div><div>both carver and &quot;nature&quot;.<br></d=
iv><div><br></div><div>Clearly the problem is no longer &quot;the tools&quo=
t;.</div><div>*I* am the problem constraining the solution.</div><div>Birth=
ing this &quot;new thing&quot; is slow, difficult, and</div><div>uncertain =
at best.</div><div><br></div><div>Tim</div><div><br></div><div>[0] Alexande=
r, Christopher &quot;Notes on the Synthesis</div><div>of Form&quot; Harvard=
 University Press 1964 <br></div><div>ISBN 0-674-62751-2</div><div><br></di=
v></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:axiomcas@g=
mail.com" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div><blo=
ckquote 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 paper... I&#39;=
m not connected to Academia<br>
so anything I&#39;d write would never make it into print.<br>
<br>
&quot;Language level parsing&quot; 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&#39;t understand Platzer&#39;s &quot;funny<br>
fraction notation&quot; (proof judgements) despite being<br>
an expert in Platzer&#39;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.=C2=A0 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&#39;s OPS5 rule based program [5],<br>
and Fahlman&#39;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&#39;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 &#39;propositional&#39; 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&#39;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 &quot;scaffolding&quot;. 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&#39;s &quot;category&quot;<br>
structure has &quot;Category&quot; things like Ring. Claiming<br>
to be a Ring brings in a lot of &quot;Signatures&quot; 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 &quot;Domain&quot; &quot;is a Ring&quot;. Category<br>
theory might provide similar structural scaffolding<br>
(eventually... I&#39;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&#39;t<br>
sufficient to say &quot;undergraduate math&quot; 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 &quot;spreading&quot;. 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>
&quot;commutative&quot; included in the code.<br>
<br>
That way, when you claim to be a &quot;Commutative Ring&quot;<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&#39;s definitions and theorems with<br>
an eye to &quot;spreading&quot; them into the group scaffold of<br>
Axiom.<br>
<br>
4) We need &quot;carriers&quot; (Axiom calls them representations,<br>
aka &quot;REP&quot;). 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 &quot;dense&quot; (all coefficients in a list),<br>
&quot;sparse&quot; (only non-zero coefficients), &quot;recursive&quot;, etc=
.<br>
<br>
A &quot;dense polynomial&quot; and a &quot;sparse polynomial&quot; 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 &quot;got this wrong&quot; because it didn&#39;t sufficiently<br>
separate the REP from the &quot;Domain&quot;. I plan to fix this.<br>
<br>
LEAN ought to have a &quot;data structures&quot; 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 &quot;Domains&quot; (in Axiom speak). That is, we<br>
need a box that holds all of the functions that implement<br>
a &quot;Domain&quot;. For example, a &quot;Polynomial Domain&quot; would<br=
>
hold all of the functions for manipulating polynomials<br>
(e.g polynomial multiplication). The &quot;Domain&quot; box<br>
is a dependent type that:<br>
<br>
=C2=A0 A) has an argument list of &quot;Categories&quot; that this &quot;Do=
main&quot;<br>
=C2=A0 =C2=A0 =C2=A0 box inherits. Thus, the &quot;Integer Domain&quot; inh=
erits<br>
=C2=A0 =C2=A0 =C2=A0 the definitions and axioms from &quot;Commutative&quot=
;<br>
<br>
=C2=A0 =C2=A0 =C2=A0Functions in the &quot;Domain&quot; box can now assume<=
br>
=C2=A0 =C2=A0 =C2=A0and use the properties of being commutative. Proofs<br>
=C2=A0 =C2=A0 =C2=A0of functions in this domain can use the definitions<br>
=C2=A0 =C2=A0 =C2=A0and proofs about being commutative.<br>
<br>
=C2=A0 B) contains an argument that specifies the &quot;REP&quot;<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0(aka, the carrier). That way you get all of the<=
br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0functions associated with the data structure<br>
=C2=A0 =C2=A0 =C2=A0 available for use in the implementation.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 Functions in the Domain box can use all of<br>
=C2=A0 =C2=A0 =C2=A0 the definitions and axioms about the representation<br=
>
=C2=A0 =C2=A0 =C2=A0 (e.g. NonNegativeIntegers are always positive)<br>
<br>
=C2=A0 C) contains local &quot;spread&quot; definitions and axioms<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0that can be used in function proofs.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 For example, a &quot;Square Matrix&quot; domain would<=
br>
=C2=A0 =C2=A0 =C2=A0 have local axioms that state that the matrix is<br>
=C2=A0 =C2=A0 =C2=A0 always square. Thus, functions in that box could<br>
=C2=A0 =C2=A0 =C2=A0 use these additional definitions and axioms in<br>
=C2=A0 =C2=A0 =C2=A0 function proofs.<br>
<br>
=C2=A0 D) contains local state. A &quot;Square Matrix&quot; domain<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0would be constructed as a dependent type that<br=
>
=C2=A0 =C2=A0 =C2=A0 =C2=A0specified the size of the square (e.g. a 2x2<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0matrix would have &#39;2&#39; as a dependent par=
ameter.<br>
<br>
=C2=A0 E) contains implementations of inherited functions.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0A &quot;Category&quot; could have a signature fo=
r a GCD<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0function and the &quot;Category&quot; could have=
 a default<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0implementation. However, the &quot;Domain&quot; =
could<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0have a locally more efficient implementation whi=
ch<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0overrides the inherited implementation.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 Axiom has about 20 GCD implementations that<br>
=C2=A0 =C2=A0 =C2=A0 differ locally from the default in the category. They<=
br>
=C2=A0 =C2=A0 =C2=A0 use properties known locally to be more efficient.<br>
<br>
=C2=A0 F) contains local function signatures.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 A &quot;Domain&quot; gives the user more and more uniq=
ue<br>
=C2=A0 =C2=A0 =C2=A0 functions. The signature have associated<br>
=C2=A0 =C2=A0 =C2=A0 &quot;pre- and post- conditions&quot; that can be used=
<br>
=C2=A0 =C2=A0 =C2=A0 as assumptions in the function proofs.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 Some of the user-available functions are only<br>
=C2=A0 =C2=A0 =C2=A0 visible if the dependent type would allow them<br>
=C2=A0 =C2=A0 =C2=A0 to exist. For example, a general Matrix domain<br>
=C2=A0 =C2=A0 =C2=A0 would have fewer user functions that a Square<br>
=C2=A0 =C2=A0 =C2=A0 Matrix domain.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 In addition, local &quot;helper&quot; functions need t=
heir<br>
=C2=A0 =C2=A0 =C2=A0 own signatures that are not user visible.<br>
<br>
=C2=A0 G) the function implementation for each signature.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0This is obviously where all the magic happens<br=
>
<br>
=C2=A0 H) the proof of each function.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0This is where I&#39;m using LEAN.<br>
<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0Every function has a proof. That proof can use<b=
r>
=C2=A0 =C2=A0 =C2=A0 =C2=A0all of the definitions and axioms inherited from=
<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0the &quot;Category&quot;, &quot;Representation&q=
uot;, the &quot;Domain<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0Local&quot;, and the signature pre- and post-<br=
>
=C2=A0 =C2=A0 =C2=A0 =C2=A0conditions.<br>
<br>
=C2=A0 =C2=A0I) literature links. Algorithms must contain a link<br>
=C2=A0 =C2=A0 =C2=A0 to at least one literature reference. Of course,<br>
=C2=A0 =C2=A0 =C2=A0 since everything I do is a Literate Program<br>
=C2=A0 =C2=A0 =C2=A0 this is obviously required. Knuth said so :-)<br>
<br>
<br>
LEAN ought to have &quot;books&quot; or &quot;pamphlets&quot; 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>
=C2=A0 =C2=A0 This is where the systems can differ significantly.<br>
=C2=A0 =C2=A0 Axiom and LEAN both have GCD but they use<br>
=C2=A0 =C2=A0 that for different purposes.<br>
<br>
=C2=A0 =C2=A0 I&#39;m trying to connect LEAN&#39;s GCD and Axiom&#39;s GCD<=
br>
=C2=A0 =C2=A0 so there is a &quot;computational mathematics&quot; idea that=
<br>
=C2=A0 =C2=A0 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 &quot;down to the metal&quot; 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&#39;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 &quot;Chapter on TLA+&quot;<br>
in &quot;Software Specification Methods&quot;<br>
<a href=3D"https://www.springer.com/gp/book/9781852333539" rel=3D"noreferre=
r" target=3D"_blank">https://www.springer.com/gp/book/9781852333539</a><br>
(I no longer have CMU library access or I&#39;d send you<br>
the book PDF)<br>
<br>
[1] <a href=3D"https://www.tul.com.tw/productspynq-z2.html" rel=3D"noreferr=
er" 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"norefe=
rrer" target=3D"_blank">https://www.youtube.com/watch?v=3DdCuZkaaou0Q</a><b=
r>
<br>
[3] &quot;ARTIFICIAL INTELLIGENCE MARKUP LANGUAGE&quot;<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=
/v19n4/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.cm=
u.edu/articles/journal_contribution/OPS5_user_s_manual/6608090/1</a><br>
<br>
[6] Scott Fahlman &quot;SCONE&quot;<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"_b=
lank">[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&#39;ve read or<br>
&gt; that have had an indirect influence on Axiom.<br>
&gt;<br>
&gt; Credit is &quot;the coin of the realm&quot;. It is easy to share and w=
rong<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&#39;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-turin=
g-award-deep-learning.html" rel=3D"noreferrer" target=3D"_blank">https://pe=
ople.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 =
was to recognize<br>
&gt; and associated 3D chemical drawings with their drug counterparts.<br>
&gt; I used Rumelhart, and McClelland&#39;s books. These books contained<br=
>
&gt; quite a few ideas that seem to be &quot;new and innovative&quot; among=
 the<br>
&gt; machine learning crowd... but the books are from 1987. I don&#39;t bel=
ieve<br>
&gt; I&#39;ve seen these books mentioned in any recent bibliography.<br>
&gt; <a href=3D"https://mitpress.mit.edu/books/parallel-distributed-process=
ing-volume-1" rel=3D"noreferrer" target=3D"_blank">https://mitpress.mit.edu=
/books/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 &quot;How Reliable is Scientific Software?&quot;=
<br>
&gt;&gt; <a href=3D"https://neverworkintheory.org/2021/09/25/how-reliable-i=
s-scientific-software.html" rel=3D"noreferrer" target=3D"_blank">https://ne=
verworkintheory.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&quot;<br>
&gt;&gt;<br>
&gt;&gt;=C2=A0 [Hatton1994], is now a quarter of a century old, but its con=
clusions<br>
&gt;&gt; are still fresh. The authors fed the same data into nine commercia=
l<br>
&gt;&gt; geophysical software packages and compared the results; they found=
<br>
&gt;&gt; that, &quot;numerical disagreement grows at around the rate of 1% =
in<br>
&gt;&gt; average absolute difference per 4000 fines of implemented code, an=
d,<br>
&gt;&gt; even worse, the nature of the disagreement is nonrandom&quot; (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]" tar=
get=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt; I should note that the lastest board I&#39;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&#39;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]"=
 target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt; I&#39;m familiar with most of the traditional approaches<b=
r>
&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 ty=
pe<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)<b=
r>
&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<b=
r>
&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<=
br>
&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 relev=
ant<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).<b=
r>
&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 &quot;trust down to the metal&quot;). (Note that Inte=
l<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&#39;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<b=
r>
&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&#39;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/bo=
okvolbib.pdf" rel=3D"noreferrer" target=3D"_blank">https://github.com/daly/=
PDFS/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:axiomcas@gmail.=
com" 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/"=
 rel=3D"noreferrer" target=3D"_blank">http://www.straightrunning.com/XmingN=
otes/</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&#39;t work on WSL2. I don&#39;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 &quot;PATH=3D/usr/lib/axiom-20170501/bin:$PATH&=
quot;<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 4 WSL2) create a .axiom.input file to include startup =
cmds:<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 &quot;/mnt/c/yourpath&quot;<br>
&gt;&gt;&gt;&gt;&gt; )sys pwd<br>
&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt; 5 WSL2) create a &quot;myaxiom&quot; command that sets=
 the<br>
&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 =C2=A0DISPLAY variable and starts axiom<b=
r>
&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-=
powershell-script-when-you-open-powershell" rel=3D"noreferrer" target=3D"_b=
lank">https://superuser.com/questions/886951/run-powershell-script-when-you=
-open-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@gm=
ail.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 =
the SANE version<br>
&gt;&gt;&gt;&gt;&gt;&gt; of Axiom as flexible as possible, decoupling mecha=
nism from theory.<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; An interesting publication by Brian Cantwell Smith=
 [0], &quot;Reflection<br>
&gt;&gt;&gt;&gt;&gt;&gt; and Semantics in LISP&quot; seems to contain inter=
esting ideas related<br>
&gt;&gt;&gt;&gt;&gt;&gt; to our goal. Of particular interest is the ability=
 to reason about<br>
&gt;&gt;&gt;&gt;&gt;&gt; and<br>
&gt;&gt;&gt;&gt;&gt;&gt; perform self-referential manipulations. In a depen=
dently-typed<br>
&gt;&gt;&gt;&gt;&gt;&gt; system it seems interesting to be able &quot;adapt=
&quot; 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;=C2=A0 =C2=A0 &quot;We show how a computational sys=
tem can be constructed to<br>
&gt;&gt;&gt;&gt;&gt;&gt; &quot;reason&quot;,<br>
&gt;&gt;&gt;&gt;&gt;&gt; effectively<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 and consequentially, about its own in=
ferential processes. The<br>
&gt;&gt;&gt;&gt;&gt;&gt; analysis proceeds in two<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 parts. First, we consider the general=
 question of computational<br>
&gt;&gt;&gt;&gt;&gt;&gt; semantics, rejecting<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 traditional approaches, and arguing t=
hat the declarative and<br>
&gt;&gt;&gt;&gt;&gt;&gt; procedural aspects of<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 computational symbols (what they stan=
d 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;=C2=A0 =C2=A0 analysed independently, in order that=
 they may be coherently<br>
&gt;&gt;&gt;&gt;&gt;&gt; related. Second, we<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 investigate self-referential behavior=
 in computational processes,<br>
&gt;&gt;&gt;&gt;&gt;&gt; and show how to embed an<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 effective procedural model of a compu=
tational calculus within that<br>
&gt;&gt;&gt;&gt;&gt;&gt; calculus (a model not<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 unlike a meta-circular interpreter, b=
ut connected to the<br>
&gt;&gt;&gt;&gt;&gt;&gt; fundamental operations of the<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 machine in such a way as to provide, =
at 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;=C2=A0 =C2=A0 descriptions of the state of that com=
putation, for inspection and<br>
&gt;&gt;&gt;&gt;&gt;&gt; possible modification). In<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 terms of the theories that result fro=
m these investigations, we<br>
&gt;&gt;&gt;&gt;&gt;&gt; present a general architecture<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 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;=C2=A0 =C2=A0 subject domain, and dealing with thei=
r 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;=C2=A0 =C2=A0 An instance of the general solution i=
s 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;=C2=A0 =C2=A0 language. Specifically, we present th=
ree successive dialects of<br>
&gt;&gt;&gt;&gt;&gt;&gt; LISP: 1-LISP, a distillation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 current practice, for comparison purp=
oses; 2-LISP, a dialect<br>
&gt;&gt;&gt;&gt;&gt;&gt; constructed in terms of our<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 rationalised semantics, in which the =
concept of evaluation is<br>
&gt;&gt;&gt;&gt;&gt;&gt; rejected in favour of<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 independent notions of simplification=
 and reference, and in which<br>
&gt;&gt;&gt;&gt;&gt;&gt; the respective categories<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 of notation, structure, semantics, an=
d behaviour are strictly<br>
&gt;&gt;&gt;&gt;&gt;&gt; aligned; and 3-LISP, an<br>
&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 extension of 2-LISP endowed with refl=
ective powers.&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt; Axiom SANE builds dependent types on the fly. The =
ability 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 =
tower 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=
 algorithm 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 =
efforts is to build<br>
&gt;&gt;&gt;&gt;&gt;&gt; &quot;all the way down to the<br>
&gt;&gt;&gt;&gt;&gt;&gt; metal&quot;. If each layer is constructed on top o=
f previous proven layers<br>
&gt;&gt;&gt;&gt;&gt;&gt; and the new layer<br>
&gt;&gt;&gt;&gt;&gt;&gt; can &quot;reach below&quot; to lower layers then t=
he 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 &quot;Reflection and Se=
mantics in LISP&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt; POPL &#39;84: Proceedings of the 11th ACM SIGACT-S=
IGPLAN<br>
&gt;&gt;&gt;&gt;&gt;&gt; ymposium on Principles of programming languagesJan=
uary 1<br>
&gt;&gt;&gt;&gt;&gt;&gt; 984 Pages 23=E2=80=9335<a href=3D"https://doi.org/=
10.1145/800017.800513" rel=3D"noreferrer" target=3D"_blank">https://doi.org=
/10.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:axiomca=
[email protected]" target=3D"_blank">[email protected]</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Having spent time playing with hardware it is =
perfectly clear that<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; future computational mathematics efforts need =
to 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&#39;ve spent a fair bit of time thinking abo=
ut structuring Axiom to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; be parallel. Most past efforts have tried to f=
ocus on making a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; particular algorithm parallel, such as a matri=
x 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=
 make each domain<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; run in parallel. A computation crosses multipl=
e domains so a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; particular computation could involve multiple =
parallel copies.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; For example, computing the Cylindrical Algebra=
ic Decomposition<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; could recursively decompose the plane. Indeed,=
 any tree-recursive<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; algorithm could be run in parallel &quot;in th=
e large&quot; by creating new<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; running copies of the domain for each sub-prob=
lem.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So the question becomes, how does one manage t=
his?<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; A similar problem occurs in robotics where one=
 could have multiple<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; wheels, arms, propellers, etc. that need to ac=
t 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 =
are ROSCORE,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; TOPICS with publish/subscribe, and SERVICES wi=
th request/response.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; These are communication paths defined between =
processes.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; ROS2 has a &quot;roscore&quot; which is basica=
lly a phonebook of &quot;topics&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; Any process can create or look up the current =
active topics. eq:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 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 basi=
cally a typed data<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; structure), e.g the topic /hw with the String =
data &quot;Hello World&quot;.<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;=C2=A0 =C2=A0 rostopic pub /hw std_msgs/String =
&quot;Hello, World&quot;<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.=C2=A0 eg:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;=C2=A0 =C2=A0 rostopic echo /hw=C2=A0 =C2=A0=3D=
=3D&gt; &quot;Hello, World&quot;<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 an=
d 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.=
 It could provide<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; services, one for each function. Any other pro=
cess 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 wa=
iting for responses<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; or continuing while the response is being comp=
uted.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; The output could be sent anywhere, to a termin=
al, to a browser,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; to a network, or to another process using the =
publish/subscribe<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; protocol, potentially all at the same time sin=
ce 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 b=
y announcing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; themselves as new &quot;topics&quot; and could=
 be dynamically 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-=
level parallelism.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; It is very effective in the robot world and I =
think it might be a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; good structuring mechanism to allow computatio=
nal mathematics<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; to take advantage of multiple processors in a =
disciplined 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 ru=
n 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 indepe=
ndent of the others.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; So if we want to use BLAS Fortran code, it cou=
ld just be another<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt; service node. In fact, any &quot;foreign funct=
ion&quot; could 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 &quo=
t;by node&quot;.<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:axio=
[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 ty=
pes. Deciding when<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; two types are equivalent may involve compu=
tation. See<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Christiansen, David Thrane &quot;Checking =
Dependent Types with<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Normalization by Evaluation&quot; (2019)<b=
r>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; This puts an interesting constraint on bui=
lding types. The<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; constructed types has to export a function=
 to decide if a<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; given type is &quot;equivalent&quot; to it=
self.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The notion of &quot;equivalence&quot; migh=
t involve category ideas<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of natural transformation and univalence. =
Sigh.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; That&#39;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:=
[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&#39;=
s eyes and expectations adapt<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to the tools they use. For instance, I=
 use emacs and expect to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; work directly in files and multiple bu=
ffers. 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=
 to &quot;get in the way&quot;. 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=
 try 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 &quot;too =
sparse&quot; for programming.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Recently I&#39;ve been working in a sp=
arse programming environment.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I&#39;m exploring the question of runn=
ing a proof checker in an FPGA.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The FPGA development tools are painful=
 at best and not intuitive<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; since you SEEM to be programming but y=
ou&#39;re actually describing<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; hardware gates, connections, and timin=
g. This is an environment<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; where everything happens all-at-once a=
nd all-the-time (like the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; circuits in your computer). It is the =
&quot;assembly language of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; circuits&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Naturally, my eyes have adapted to thi=
s 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&#39;m normally doing lite=
rate programming 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 t=
o 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=
 to be a &quot;sea of parens&quot;.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Yet as a lisp programmer, I don&#39;t =
even see 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 d=
ocument to adapt vision to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; see the latex / lisp combination as na=
tural. The latex markup,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; like the lisp parens, eventually just =
disappears. 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 q=
uickly adapt. The upside<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; is that there is always a &quot;finish=
ed&quot; document that describes the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; state of the code. The overhead of wri=
ting a paragraph to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; describe a new function or change a pa=
ragraph 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 =
to generate a current PDF<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; and then I extract, load, and execute =
the code. This loop catches<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; errors in both the latex and the sourc=
e 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=
 in the document after every<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; run of make. That way I can edit the b=
ook 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 boo=
k while writing the code is<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; more productive. I don&#39;t have to r=
emember 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=
 and 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 &quot;raw code&q=
uot; programming.<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"ma=
ilto:[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 interes=
ting property of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;Living within the compiler&q=
uot;.<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 syst=
ems that present themselves<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; through the Read-Eval-Print-Loop (=
REPL) allow the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; ability to deeply interact with th=
e 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 soft=
ware 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.georgef=
airbanks.com/videos/" rel=3D"noreferrer" target=3D"_blank">https://www.geor=
gefairbanks.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 involv=
es the ability to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; dynamically define categories, rep=
resentations, and functions<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; along with &quot;composition funct=
ions&quot; that 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 handli=
ng polynomials. There are<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; a lot of choices, depending on you=
r use case. You might want<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; different representations. For exa=
mple, you might want dense,<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; sparse, recursive, or &quot;machin=
e compatible fixnums&quot; (e.g. to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; interface with C code). If these d=
on&#39;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 &quot;lego-li=
ke&quot; building blocks require careful<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; thought about creating &quot;fully=
 factored&quot; 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 b=
arrier of &quot;compiler&quot; vs<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;interpreter&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; does not seem useful. It is better=
 to &quot;live within the compiler&quot;<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 th=
ings &quot;on the fly&quot;.<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 go=
ing to want an associated<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; proof of the functions you create =
along with the other parts<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; such as its category hierarchy and=
 representation 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=
 job. :-)<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;=
 wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The Axiom SANE compiler / inte=
rpreter 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=
 and 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 constructi=
on of code as well as dynamic type<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; construction at runtime. Both =
of 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 mixt=
ure 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 re=
solution 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 =
not 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 &quot;prefix thunk&quot; tha=
t will perform 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 nee=
d 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 co=
mpile time that the types are both<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; bounded-NNI and the result is =
bounded-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 +=
 at runtime. If not, we might have<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; + applied to NNI and POLY(FLOA=
T), which requires a thunk to<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; resolve types. The thunk could=
 even &quot;specialize and compile&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; the code before executing it.<=
br>
&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 im=
plementation of<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;threaded-interpreted&quo=
t;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; languages model provides an ef=
ficient 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 &quot;i=
nserted&quot; in intermediate thunks.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; The model also supports dynami=
c 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=
 with low-level threading gives an<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; easy to understand and robust =
design.<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. &quot;Threa=
ded Interpretive Languages&quot; (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 hre=
f=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; I&#39;ve worked hard to ma=
ke Axiom depend on almost no other<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; tools so that it would not=
 get caught by &quot;code rot&quot; 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&#39;m also tryi=
ng to make the new SANE version much<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; easier to understand and d=
ebug.To that end I&#39;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 v=
iew 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 =
possibly 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=
 gets 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 real=
ly 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 th=
e gcd function from NNI, there is the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; representation of the gcd =
function 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 t=
he 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 associa=
ted 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 inheri=
ts 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 an=
d 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 i=
s 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 =
code won&#39;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 th=
ese structures. I&#39;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 t=
oo weak. Either everything has to be<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;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 gra=
ph&quot; or &quot;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&quot;. Plus, construc=
ting dynamic 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=
 new 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 proble=
m of keeping the browser &quot;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&quot;. So =
something 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=
 into 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=
 associated 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-f=
riendly 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 liter=
ate 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 f=
orm 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&#39;d like =
to have the ability to &quot;deep dive&quot; 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 de=
bugging, 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 =
they 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 com=
putation.<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&#39;m lookin=
g at using 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 w=
ould 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 mod=
ify) 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 tha=
t 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&#3=
9;s all 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&#39;t new=
. They 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 platfor=
m 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 th=
e talk<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;The Unreasonable=
 Effectiveness 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&quot;<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href=3D"https://vim=
eo.com/74354480" rel=3D"noreferrer" target=3D"_blank">https://vimeo.com/743=
54480</a><br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; which questions whethe=
r 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 &=
lt;<a href=3D"mailto:[email protected]" target=3D"_blank">[email protected]=
om</a>&gt; wrote:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; Peter Naur wrote a=
n article of interest:<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; <a href=3D"http://=
pages.cs.wisc.edu/~remzi/Naur.pdf" rel=3D"noreferrer" target=3D"_blank">htt=
p://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 =
mirrors my notion that Axiom needs<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; to embrace literat=
e programming so that the &quot;theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the problem&quo=
t; is presented as well as the &quot;theory<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; of the solution&qu=
ot;. 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, t=
o 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=
 designing and coding a program.<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; I refer to it regu=
larly when discussing how much<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; documentation to c=
reate, how to pass along tacit<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; knowledge, and the=
 value of the XP&#39;s metaphor-setting<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; exercise. It also =
provides a way to examine a methodolgy&#39;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, wh=
ich follows, note that the quality of the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; designing programm=
er&#39;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 =
his 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. N=
ote that the quality of a later<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; programmer&#39;s<b=
r>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; work is related to=
 the match between his theories and the<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; previous programme=
r&#39;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&#39;s i=
deas, the designer&#39;s job is not to pass along<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; &quot;the design&q=
uot; but to pass along &quot;the theories&quot; 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=
 more useful and more appropriate. It also<br>
&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt; highlights that kn=
owledge 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 t=
he 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 knowledg=
e.<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>

--000000000000cf249d05da14f883--