[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Proving Axiom Correct

From: Martin Baker
Subject: Re: [Axiom-developer] Proving Axiom Correct
Date: Mon, 2 Apr 2018 21:34:45 +0100
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0


I've been experimenting with a language called 'Idris'. I've been playing around with writing some of the Axiom SPAD library code in Idris. My code so far is here:
Nothing usable yet, I'm just experimenting with whats involved.

So in the same way that Coq is a proof assistant which can generate some code by Curry-Howard then Idris reverses that and starts with the algebra code and allows that to be linked to proofs (which are types).

Idris is based on Haskell but with 2 very important differences which make it very compatible with SPAD: * It has full dependent types built into the language from the start. (not a plugin like Haskell)
* It is eager, not lazy, by default.

Of course the language is pure functional so translating imperative code is hard but its an approach that interests me, I would be interested to hear what you think.


On 02/04/18 18:37, Tim Daly wrote:
I've been working on proving Axiom correct for years now.

I've spent the last 18 months learning proof systems and
deep-diving into the theory (thanks, in part, to Carnegie
Mellon's Computer Science Department giving me the
"Visiting Scholar" appointment and faculty access).

I've "discovered" that there are two large, independent,
and largely parallel efforts in computational mathematics.

There is the computer algebra field, where we spend most
of our time and effort. The concentration is on finding new
algorithms. This is interesting and quite satisfying. It appears
to be "progress". There is a large body of literature.

There is the program proof field, where a large number of
people spend most of their time and effort. The concentration
is on building systems to prove programs correct. On some
occasions a computer algebra algorithm, like Groebner basis,
is proven. There is a large body of literature.

Surprisingly though, there is little overlap. It is very rare to
find a paper that cites both Jenks (CA) and Nipkow (PP).

In fact, without a great deal of background, the papers in the
program proof field are unreadable, consisting mostly of
"judgements" written in greek letters. Or, coming from the
proof field, finding the computer algebra "algorithms" lacking
anything that resembles rigor, not to mention explanations.

Both fields are very large, very well developed, and have been
growing since the latter half of the last century.

It is important to bridge the gap between these two field.
It is unlikely that anyone will invest the millions of dollars and
thousands of hours necessary to "rebuild" an Axiom-sized
computer algebra system starting with a proof system. It is
also unlikely that anyone will succeed in proving most of
the existing computer algebra systems because of their
ad hoc, "well-it-mostly-works", method of development.

Axiom has the unique characteristic of being reasonably well
structured mathematically. It has many of the characteristics
found in proof-system idea like typeclasses (aka Axiom's
"Category-and-Domain" structures. What Axiom lacks is the
propositions from typeclass-like systems.

So the path forward to unite these fields is to develop the
propositional structure of Axiom and used these propositions
to prove the existing algorithms. Uniting these fields will bring
a large body of theory to computer algebra and a large body
of algorithms to a grounded body of logic.


Axiom-developer mailing list

reply via email to

[Prev in Thread] Current Thread [Next in Thread]