Re: Proving Axiom Correct

Tim,

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:
https://github.com/martinbaker/Idris-dev/tree/algebra/libs/algebra
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.

Martin

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.
> 
> Tim
> 
> 
> 
> 
> 
> _______________________________________________
> Axiom-developer mailing list
> [email protected]
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>