Wolfram works with the full mathematical expression tree. It works very well in practice but the equality test is undecidable in general.

Yes, I should have written "practical programming language". It definitely possible to resolve many equations like this (though not all of them), but is quite a slow process, which is ok for a math system like Mathematica, but not for a real-life programming language.

"Real-life programming language" or "practical programming language" assumes that there's only one acceptable set of trade-offs for all "real-life" or "practical" problems. I suspect that what you actually meant was "a programming language designed to create industrial-strength consumer or business software".

As one of the maintainers has noted repeatedly on this thread, Pyret is a "real-life programming language" whose purpose is educational. Mathematica is a "real-life programming language" whose purpose is solving math equations. Performance isn't much of an issue in either case, so it's a perfectly acceptable trade-off.

That these languages weren't designed with your use case in mind doesn't make them illegitimate or inferior languages.