I agree, and discussed this a little. There is one key difference with the theorem provers- many of them share this lofty goal of building a library, akin to a

I agree, and discussed this a little. There is one key difference with the theorem provers- many of them share this lofty goal of building a library, akin to a 'library of Alexandria' (The article discusses this vision, and the research project I linked to at Cambridge is called 'Alexandria'). It's a grand vision - to formalise all mathematical knowledge in a library. This vision doesn't exist in the world of regular software. Nobody to my mind has claimed they're building a library of Alexandria. You could make the claim for npm, but I might shed a tear if you did that.