Re: Permission to quote

[Tim Daly]

I did a survey of a couple hundred papers from the computer
algebra and proof camps. The only person mentioned in both
bibliographies on a regular basis seems to be James Davenport.

All attempts at combining the systems seems to be either a
simple cover (e.g. a simple front-end on Mathematica) or a
single proof (e.g. Buchberger's Groebner Basis algorithm).

The other approach is "arms length", either by directly sending
results or creating an "island" of "math facts" that translates
from one area to another.

Your effort was one of the very few that tried a direct embedding.

My approach is to create extensions for specification (e.g.
ensures, requires, forall, given-when-then, etc.), and know
how to propagate definitions and axioms in the categories.

The domains also have their specific axioms. The representation
has its own axioms. All of which form an environment for a
function specification and proof.

Proofs are their own "first-class" objects that can be passed,
constructed dynamically, and, hopefully able to re-generate
code. The ideal is that code A is used to construct proof B
which can be used to re-generate code A, ,showing "round
trip" behavior.

The same environment will be available to the user in the
interpreter.

At the moment I'm collecting "background" research in volume
13 on the specific case of the GCD algorithm (of which Axiom
seems to have 22 (e.g. NNI, poly GCD, etc.). There is a lot to
know.

The SANE compiler is in volume 15. (The bibliography volume
will give you some idea of the extent of the research so far.)

Both are "a work in progress" and active research. The fact that
I'm doing it all "in the open" makes it seem chaotic and confused.
But if I knew how to solve the problems it wouldn't be research.

There is no such thing as a simple job.

Hope you and your family are healthy.

Tim

PS. This research is the most fun I've ever had.
It has become my "iron rice bowl"
https://en.wikipedia.org/wiki/Iron_rice_bowl