> Pretty much the only systems that more or less get math right are the mathematical libraries for proof assistants (Lean, Coq, etc.). The mathematical structures and interfaces in Lean's MathLib are actually pretty close to what I'd like to see in a CAS.
This comes with HUGE practical disadvantages. Yes, it would be possible to use type theory to make a mathematically rigorous CAS, but it would never be practical. Anyone who has ever tried knows that even proving something trivial like a+b+c+d=d+b+c+a in a theorem prover requires a suprising amount of ingenuity. There are few people in the world who have the skills to define and prove something more advanced like Buchberger's algorithm, and a task like that would probably require several math papers worth of new research just to produce the slowest implementation known to mankind. And it would take years.
This comes with HUGE practical disadvantages. Yes, it would be possible to use type theory to make a mathematically rigorous CAS, but it would never be practical. Anyone who has ever tried knows that even proving something trivial like a+b+c+d=d+b+c+a in a theorem prover requires a suprising amount of ingenuity. There are few people in the world who have the skills to define and prove something more advanced like Buchberger's algorithm, and a task like that would probably require several math papers worth of new research just to produce the slowest implementation known to mankind. And it would take years.