Re: [Axiom-developer] Knuth's literate style

[C Y]

Gabriel Dos Reis wrote:
> On Mon, 14 May 2007, C Y wrote:
>
> | I hadn't heard of association with TeX as being a detrimental factor to
> | a project.
> 
> I'm pointing at the moon, don't look at my finger.
> 
> The detrimental factor is not the association with TeX per se.
> But setting TeX as the gold standard: to be blunt, that lacks ambition and
> vision; I don't see how a research funding agency would be excited funding
> something like that in 2007.

The vision, as I understand it, is to incorporate the vast body of
mathematical knowledge that exists today in a form readily
understandable and usable both by human and computer.  How do we encode
mathematical knowledge in such a fashion that there will be no major
incentive to re-code it in the future?  What is a system design that
will scale as far as necessary?

Some related questions:

1.  How do we avoid duplicating research accidentally due to
students/researchers not having the resources to do comprehensive
literature searches?  As the body of literature keeps growing the
ability of one person to be aware of everything they could use
decreases.  How do we solve this problem?

2.  Formal correctness proofs of mathematical statements in both science
and mathematics as a default inclusion would be a considerable help in
preventing certain types of errors.  What kind of system do we need to
merge formal proof systems and computer algebra systems?  How should it
be done?  What features are needed?  What kind of system is necessary to
produce answers reliable enough for scientists to depend on them?

TeX as such is only one small part of the puzzle.  It (or something like
it) is necessary but not sufficient.  Literate programming or
developments there-of are a tool, a means to an end.  However, because
literate programming has not seen a whole lot of development we need to
implement the basic functionality before we scale beyond it.  TeX is the
"gold standard" in that it is probably the most widely known, widely
used example of literate programming in action.  It also does its job
well enough to be a standard many years after the core work was
completed.  That makes it an interesting case study as well as a tool -
its success over the long term is something to pay attention to.

To my mind, funding development on Axiom at this stage should be
properly viewed as doing groundwork for the future.  The problems we are
grappling with now are secondary - what we really want is the framework
within which mathematical research via computer can scale.

If Axiom proper is the space shuttle, right now we're working on the
platform that moves it from the warehouse to the launch pad.  Doesn't
have much to do with mathematics per say, but it's absolutely essential
infrastructure.  The exciting part comes later.

Whether this is something that should be funded, I don't know.  I would
think that a publicly available resource of this sort would be a logical
thing for a government to support - it's a type of project that
commercial organizations won't be interested in, and ideally it would
provide the same benefits for mathematical research that the highway
system does for national travel.  That's just my opinion though - I have
no detailed knowledge of the NSF/NIST funding mandates.

Cheers,
CY