Very good points. It helps to list the requirements of a system before you actually build it! I did something very similar when I wrote about what I would like

Very good points. It helps to list the requirements of a system before you actually build it! I did something very similar when I wrote about what I would like to see in an interactive theorem proving (ITP) system: https://doi.org/10.47757/practal.1 https://doi.org/10.47757/practal.1 This worked out great so far in that I managed to come up with a logic which I believe is actually the BEST logic for mathematics, Abstraction Logic (AL): https://doi.org/10.47757/pal.2 https://doi.org/10.47757/pal.2 Furthermore, I think the ideal ITP system and the ideal Computer Algebra System (CAS) are actually the same thing. Many will dispute that, but this is just because they cannot look further than the shortcomings of current incarnations of both concepts. I actually think that AL will help to unify those two concepts, as an AL term is a very simple thing, and much easier to manipulate than a typed term of some complicated type theory! A lot of the points you list are really just saying that you want your CAS to be an ITP system: a) Inert expressions b) Based on math c) Based on typed math d) Type-integrated symbolics and enclosures e) Good for Inequalities g) Large but lean h) Text-friendly (and human-friendly) Your other points are points that people want for ITP systems, too: i) Integers j) Good math display k) Well-named As for types, I believe now that a static type system just does not cut it. I believe something like Practical Types (which led me to AL) is the right way to go, such that you have semantic types, which are basically like sets, without requiring that everything is a set: https://doi.org/10.47757/practical.types.1 https://doi.org/10.47757/practical.types.1