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.