From 10a0c43355ce9e00a1ff7f2fc8dd46eb2392bb8d Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Wed, 16 Aug 2017 17:13:00 0400
Subject: [PATCH] goals  a newly added file to explain current goals

changelog  2 +
goals  186 +++++++++++++++++++++++++++++++++++++++++
patch  16 +
src/axiomwebsite/patches.html  2 +
4 files changed, 191 insertions(+), 15 deletions()
create mode 100644 goals
diff git a/changelog b/changelog
index 99b9422..c972f2a 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20170816 tpd src/axiomwebsite/patches.html 20170816.01.tpd.patch
+20170816 tpd goals  a newly added file to explain current goals
20170814 tpd src/axiomwebsite/patches.html 20170814.04.tpd.patch
20170814 tpd books/bookvolbib Axiom References in External Literature
20170814 tpd src/axiomwebsite/patches.html 20170814.03.tpd.patch
diff git a/goals b/goals
new file mode 100644
index 0000000..96bf69f
 /dev/null
+++ b/goals
@@ 0,0 +1,186 @@
+Computational Mathematics is not a competition, it is a field
+of study. Do what you can to make it better for all.
+
+Axiom has several goals.
+
+1) Axiom needs to live.
+
+Keeping Axiom alive is a primary goal. It is patently obvious that
+open source projects tend to die when the lead maintainer stops
+development for any reason. Github and Sourceforge have many
+thousands of examples.
+
+Commercial software dies when the company dies. Witness
+Symbolics (Macsyma), Soft Warehouse (Derive), or MapleSoft
+(Maple was sold to a Japanese company which currently
+supports it). Companies die, on average, after 15 years.
+
+Axiom is timeless in that it is computational mathematics. The
+algorithms and results will always be correct. So unlike other
+efforts, what we write can be used by later generations.
+
+This goal influences every decision about direction and purpose,
+in particular, driving some of the goals listed below.
+
+2) Axiom needs to be better documented and better explained.
+
+The decision to deeply explain and document Axiom is based on
+the obvious need to make it possible for new people to maintain,
+modify, and extend it.
+
+Explanation needs structure so a new person can "linearly learn"
+what is needed. It also needs structure so information can be found
+easily through some search mechanism. It further needs structure to
+incorporate what is already known.
+
+Literate programming was chosen after a long search for possbile
+solutions.
+
+The booklike nature of a literate program focuses attention on
+people, not machines. It is a linear format which provides a way
+to communicate ideas using methods developed over history.
+Books are structure we understand.
+
+You can find information in the volume choice; there are currently
+21; the table of contents, tables of figures and subjects, detailed
+indexes, a new "rich form bibliography" which includes abstracts,
+and the use of hyperlinks between volumes, to outside sources,
+and to youtube videos and courses. Experiments are being done
+to embed gifs to illustrate ideas.
+
+Algorithms, Categories, and Domains now have hyperlinks to
+published literature and there are some initial examples of deeper
+documentation of the algorithms. Ideally every algorithm will provide
+sufficient explanation of the implementation or links to explanations
+so the implementation can be understood in context.
+
+In additon, people have generously contributed material from other
+sources which directly explain details of Axiom, sometimes even
+written by the Axiom primary authors.
+
+There is a structured bibliography based on various subtopics as
+well as a section on external references to Axiom (currently 636
+have been found).
+
+There is an automated regression test suite that is being expanded
+and made uniform for testing all known functions. The Axiom code
+is now using a uniform syntax and has perfunction help text, as
+well as automated generation of help files.
+
+Finally there is a literate bug document that points at known
+problems (with a plan for adding deeper explanations and possible
+solutions).
+
+3) Axiom is RESEARCH software.
+
+It is exploring ways to push the boundaries of computational
+mathematics.
+
+3A) Proving Axiom Correct
+
+Computational Mathematics IS Mathematics.
+It needs proofs, not handwaving.
+
+This effort involves adding proof technology to Axiom.
+Propositions are types and can be incorporated into the Category
+structure as "type signatures". Domains already have
+representations which is known in logic as the "carrier". Proofs
+of Propositions, using operations from the domain, will show that
+the Domain is properly designed and implemented.
+
+The three parts (signatures, representations, proofs) mirror the
+logic structure of "typeclasses" which have (signatures, carriers,
+proofs) so there is a solid formal basis in logic for Axiom's
+Category/Domain structure.
+
+Because Axiom uses Group Theory as a scaffold there is a solid
+formal basis for inheriting propositions so a Domain knows what
+it needs to prove and what operations are needed in the Domain
+to support that proof.
+
+Axiom currently can invoke Coq and ACL2 during the build process.
+An example of automatically proving a lisp algorithm using ACL2
+exists. A Coq example is being worked on. In addition, we are
+looking in detail at a new system called LEAN.
+
+3B) Number representations
+
+There are two research efforts. One involves "formal numbers" so
+that we can claim that the symbol 'x' is an 'Integer' without giving
+it a value. This was work originally performed under grant at City
+College of New York.
+
+The second involves work by Gustafson on a new representation
+of floats that can be dynamic in range and easier to reason about.
+The goal is to push this through the numeric libraries in order to
+eliminate some of the costly checking and arrive a reliable results.
+Some of this work is being done on a FPGA (which is now
+mainstream on some Intel chips).
+
+3C) Provisos
+
+Provisos are a longstanding research question. Some work has
+been done, mostly using Cylindrical Algebraic Decomposition, to
+derive new ways to constrain the boundaries of valid computations.
+It is expected that this work will benefit greatly from the integration
+with formal methods listed above.
+
+4) Teaching
+
+In order to keep Axiom alive we need to teach the next generation.
+
+Axiom is developing the coursework necessary for teaching
+computational mathematics. There are Universities planning to
+teach using Axiom and every effort will be made to support those
+efforts. In addition, there is a plan to teach at CMU.
+
+The end result will be course outlines, a set of slides for standard
+28 lecture courses, and published youtube videos collected under
+a youtube channel for distance learning.
+
+Besides computational mathematics, one of the courses will focus
+on maintaining, modifying, and extending Axiom with new ideas.
+
+5) Standards
+
+5A) Axiom has done some work to automate the semantics of
+NIST's Digital Library of Mathematical Functions (DLMF). Macros
+translate the Latex sources to Axiom input based on additional
+decorations.
+
+5B) Axiom has a Computer Algebra Test Suite (CATS) which
+uses published sources as test cases, finding bugs in Axiom
+as well as the publications.
+
+5C) Axiom is moving to full browserbased HTML5 documentation,
+moving the Hypertex and Graphics packages to HTML and Canvas
+code. Dynamic Axiom input/output in HTML exists and works.
+
+6) New Algorithms
+
+Research on new algorithms, such as a full implementation of Clifford
+algebra, are "inprocess". Gustafson Floats will eventually be
+another Domain as a numeric category, useful for constructing
+things like POLY(GUST), that is, Polynomials over Gustafson floats.
+
+New algorithms are interesting but without proper explanation of the
+idea and the implementation detail they are just "soontobedeadcode".
+
+Every effort is being made to ensure that new code provides the details
+needed to understand the algorithm and the implementation, along with
+proper testing, examples, help files, and associated external references.
+
+7) The 30 Year Horizon
+
+Axiom has a "30 Year Horizon" focus. We will arrive at our goal in 30
+years, starting today. Which is, in mathematical fashion, true for every
+given future day.
+
+Computational Mathematics is a huge field and we are only at the very
+beginning of this journey. Find an idea. Research the literature. Talk to
+a lot of people. Push the envelope just a little bit. In other words, do the
+equivalent of a PhD thesis. You already have a research platform. You
+don't need the degree, you just need the ambition.
+
+Collaborate, Cooperate, Contribute.
+
diff git a/patch b/patch
index e5b1bad..53691db 100644
 a/patch
+++ b/patch
@@ 1,16 +1,2 @@
books/bookvolbib Axiom References in External Literature

Goal: Axiom References in External Literature

\index{Smith, Robert}
\begin{chunk}{axiom.bib}
@misc{Smit12,
 author = "Smith, Robert",
 title = "Excursions in Mathematics Using Lisp",
 link = "\url{https://www.youtube.com/watch?v=nTI_djS6dI}",
 year = "2012",
 keywords = "axiomref"
}

\end{chunk}
+goals  a newly added file to explain current goals
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index e569792..05c5418 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5792,6 +5792,8 @@ books/bookvolbib add Frege Function and Concept paper
books/bookvol13 review of Cardelli (Card85) paper
20170814.04.tpd.patch
books/bookvolbib Axiom References in External Literature
+20170816.01.tpd.patch
+goals  a newly added file to explain current goals

1.9.1