Re: [Axiom-developer] Axiom's Sane redesign musings

[Martin Baker]

On 19/06/2019 12:18, Tim Daly wrote:
> The effort to
> Prove Axiom Sane involves merging computer algebra and proof
> technology so Axiom's algorithms have associated proofs.

Tim,

Are there some fundamental compromises that have to be made when 
combining computer algebra and proof technology?

For instance in proof assistants, like Coq, equations are types for 
instance:

x = x + 0

is a proposition which, by Curry-Howard, can be represented as a type. 
To prove the proposition we have to find an inhabitant of the type (Refl).

But in computer algebra I would have thought this equation would be an 
element of some Equation type (I'm skipping over a lot of details).

Do you think both of these approaches could be brought together in a 
consistent and elegant way?

Also my (limited) understanding is that Coq prevents inconsistencies 
which makes it not Turing complete and therefore cant do everything 
Axiom can do?

Martin