> A CAS worth its name ought to be able to represent structures like transcendental number fields, rings of holomorphic functions, differential fields, transseries, and so on.
Doing this in a principled way requires implementing constructive analysis, which is not easy. Even something as simple as equality of real numbers is not constructively defined, one has to work with constructive apartness relations instead.
No. Constructive analysis is not needed for this. Classical mathematics will do just fine. Stating nonsense like this is what gives constructivism a bad name. That's not saying that there is no room for constructivism in an ideal ITP/CAS system, there certainly is!
Doing this in a principled way requires implementing constructive analysis, which is not easy. Even something as simple as equality of real numbers is not constructively defined, one has to work with constructive apartness relations instead.