Re: Axiom musings...

[Tim Daly]

One of the struggles of working with first-class dependent types
is that they can be created "on the fly". Ideally, when used, the
type information can be "factored out" to yield a specialized
version that is more efficient. The idea is best described in a
book, called Partial Evaluation, which used the type information
to collapse and specialize a function.

Jones, Gomard, and Sestoft "Partial Evaluation and Automatic
Program Generation" (1993) Prentice Hall


On 12/31/20, Tim Daly <axiomcas@gmail.com> wrote:
> 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
>