OTOH do we really have to make a difference, whether a mine or a quarry cuts the stone? Can’t it all be from rocks?
I think that this is an idea worth discussing. Imagine you're a newbie playing the tutorials for the first time, would it bother you if they were both called "rock"? Or maybe we could go with "rocks" for the quarry resource and "rock" for the mountain resource?
For Empire & Barbarians both resources are the same. You will produce the same things there, so it can be named in the same way. But Atleantans have strange mines
But going to the origin: in Settlers II there were stones and granite. Two different resource names.
I don't think that for newbie it will make lots of confusion. Both ways are used in different strategy games (for any type of resources), and people are still playing them