Re: [Axiom-developer] Why proving Axiom correct is important

[Martin Baker]

On 08/05/15 10:02, address@hidden wrote:
> Axiom Volume 13 is the start of the pile. If you find any papers
> or articles that might be of interest to the goal, please let me know.

Tim,

I am currently reading Nipkow/Klien [1] just to get a top level view of 
the subject (I have not looked at any research papers).

The book is based around Isabelle/HOL so if you don't want to use 
Isabelle the book may not be of interest to you? I have only just 
started reading the book so I don't have any great insights to give.

I get the impression that what proof assistants / interactive theorem 
provers are about is proving equations/theories from other theories 
using logic and proof methods like induction. I think what you are 
talking about is proving algorithms correct (Semantics?) this is covered 
in part 2 of the book. Do you think these sort of approaches: 
Denotational Semantics, Small-step Semantics, Big-step Semantics and so 
on are what you are aiming at?

I get the impression that using a separate proof assistant is not ideal 
and there would be a lot of advantages in combining the symbolic algebra 
program (Axiom) with the logic/proof assistant. Apart from anything else 
the learning curve is as steep as Axiom! The problem for me is the 
massive and confusing overlap of these types of program. Not just the 
program but, more importantly, the libraries. As you can see from the 
libraries here:
http://isabelle.in.tum.de/dist/library/HOL/index.html
it contains most of the same algebras as Axiom but in a slightly 
different hierarchy.

A possible first step would be to encode axioms/rules/identities in each 
Axiom category/domain. If nothing else this would allow automatic 
generation of test code at random values, this is not proof but it would 
be a first step to proofs at a later stage.

Martin

[1] Concrete Semantics with Isabelle/HOL, Nipkow/Klien, 2014, ISBN 
978-3-319-10541-3