Re: Axiom musings...

[Tim Daly]

It's been a long, slow effort to "get up to speed" (or more
accurately "a slow crawl") on the various subjects one needs
to know to work on "computational mathematics" aka SANE.

A reading knowledge of a lot of areas is needed, including
things like

abstract algebra (to understand Axiom's category/domain)
type theory (to understand first-order dependent types)
proof theory (to understand Gentzen, sequents, etc.)
category theory (to understand catamorphs, functors, etc.)
metaobject protocol (to understand CLOS extensions)
number theory (to understand finite fields)
calculus (to understand field extensions for integration)
programming (to understand typeclasses, CLOS, etc)
philosophy (to understand polymorphic sets, etc)
CPU hardware (to understand "down to the metal", FPGA, etc.)
Specification (to understand consistancy, completness, etc)
Verification (to understand decision procedures, etc)
Proof tools (like Coq, Lean, etc.)

and a few other subjects that won't come to mind at the
moment.

The usual academic approach, that creates a special
"course of study", requiring classes in areas is probably
best. There are a lot of good online courses, such as
the UOregon summer school, that introduce the basic
ideas clearly. There are some good introductory books
like Troelstra and Schwichtenberg's "Basic Proof Theory"
that cover Gentsen, Hilbert, and Natural Deduction ideas.

It seems worthwhile to put together a full course of study
with links to videos and books, so one can get up to speed
on required knowledge. I'll start an outline with links to
these on the axiom-developer.org website in the coming
weeks. It's sort-of an "Axiom University" major in
computational mathematics.

(There are no degrees :-) But one does mathematics and
programming for the joy of it anyway so who cares?)

I welcome suggestions and online links.

Tim