Computer Algebra Systems (CAS) are philosophically interesting in that they are an aspect of the long history of treating mind as mechanism. In this respect, mathematics may be thought of as formalizing "mind" and CAS the closest approximation to a mechanical implementation. We routinely encounter formal expressions of mathematical identities (equivalence theorems) in the literature of mathematics yet there seems to be no current CAS that takes, as input, those formal expressions to extend their capabilities.
Instead, what we have, are implementations in variations of functional programming languages (LISP, Haskell, etc.) that seem, inevitably, to resort to procedural formalisms that rarely if ever appear among the vast edifice of mathematics. If anything, the identities that make up the bulk of mathematics are best thought of as relations as opposed to the degenerate (N:1) relations known as functions. One would have expected there to be, at the very least, a relational formal language (such as the predicate calculus) implemented as a domain specific language (DSL) -- specific to the domain of importing mathematical identities from the literature of mathematics.
People routinely interpret these mathematical identities in scientific and technical papers without remark on this as a remarkable capability. Yet it is also considered unremarkable that CAS are not extensible in terms of these same identities.
Why is this?