[yaseer]

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.