You're correct. My primary focus is on Spad code.
In a logic setting there are things called Typeclasses which are roughly
equivalent to Axiom Categories. Typeclasses have 3 parts:
signatures -- just like Axiom
carriers -- Axiom's Domain representation
propositions -- formal properties
The fact that Axiom puts carriers in the domain allows us to have multiple
instances with the same signature set (e.g. Sparse vs Dense polynomials)
The fact that Axiom lacks propsitions causes us to invent a method of
declaring properties (e.g. commutative("*") ). This was fine for the 1970s
but mathematics has gotten much more precise and mechanical about
reasoning with such properties (e.g Coq, Agda, Isabelle, etc)
Mathematics has improved but Computer Algebra is still stuck in the
ad-hoc, informal rewrite semantics. It is time to use these research
results to improve Computer Algebra. Axiom has an excellent structure
based on Group theory which makes this feasible.
The Curry-Howard isomorphism is that propositions are types. That means
that propositions are part of the type declarations that should be in Axiom.
So instead of declaring 'commutative' we add the proposition stating the
commutative property to the appropriate Category.
Given a domain, e.g. NNI, we should be able to collect all of the
propositions
it inherits from the Category chain and use them to prove properties of the
algorithms in the NNI domain, such as GCD(x,y) = GCD(y,x). Domain
specific properties can be added at the Domain level.
So step 1 is to decorate the categories with propositions. Which means that
step 0 is to be able to encode and distribute propostions. Which means that
step -1 is to figure out how to parse, represent, and manipulate
propostions.
step -2 is to see what has been done before in this area.
step -3 is to create a survey article... which is what I've been working on
and hope to publish before the end of this semester.
Prior efforts seems to be mostly about CA and Proof systems running
in parallel and communicating in order to provide user-level proofs.
I'm trying to unify the two areas of mathematics into a single,
consistent system where system level proofs provide trusted results.
That said, the work still needs to be grounded with lisp-level proofs
since Axiom relies heavily on lisp-level primitives like List types.
I've proven one of the lisp functions so far (using ACL2). I'm adding
type signatures to the lisp code and rewriting functions to be strongly
typed (and more in line with a functional programming style).
At the moment, during build Axiom calls ACL2 for the lisp proofs and
Coq for the Spad proofs (the first of which is still under construction).
Carnegie Mellon University has been exceptionally generous in giving
me access to logic courses (quite a few in the CS department these days).
I get to ask questions of professors who have pioneered logic research.
Tim
On Sat, Nov 4, 2017 at 4:38 AM, Martin Baker <ax87...@martinb.com> wrote:
> On 04/11/17 00:42, Tim Daly wrote:
>
>> On the other hand, my current effort involves proving Axiom correct. That
>> should (in theory) eliminate whole classes of errors. This is at the
>> expense
>> of proving new code correct which tends to get a negative reaction from
>> developers.
>>
>
> Tim,
>
> I know little about proving code correct (though it looks like an
> interesting topic) so I'm certainly not doubting anything you say. Its just
> that (in my ignorance) I would have thought it would have been easier to
> prove high level code correct than low level code and therefore, for this
> reason, better to move boot code to SPAD than Lisp?
>
> By 'high level code' I mean code with meaningful static types and
> semantics closer to mathematical structures.
>
> Martin B
>
>
>
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer
