Yes, that’s why in the tracer it’s planned to not do automatic evaluation, as described in Symbolic sqrt(2) and sin(pi) - #21 by ChrisRackauckas, with dispatches for alternative constructor-based simplifications all being type based.
That’s a good idea.
That is what we do. Sounds like Symbolics.jl is on the right path then, thanks.