[Tainnor]

Yeah, Big-O notation is only part of the picture and yes, "galactic algorithms" that are theoretically efficient but only for astronomically big inputs do exist, but in many cases (especially if your algorithm isn't doing anything particularly deep or clever) linear is faster than quadratic which is faster than exponential on real world input, too.

Mathematics is the science of modeling and abstraction and that abstraction exists in order to make the process of knowledge gathering easier. It works very well for the sciences, so I would say the method has been proven. Of course, if the models turn out to be completely inappropriate, that would be different, but so far, the simple machine models used (implicitly or explicitly) in the analysis of algorithms seem to be rather reasonable.

The alternative that you suggest, trying to benchmark concrete implementations of algorithms has so many confounders that it would be very hard to execute properly. I'm sure people are doing this too, but the formal Big O proof has a different quality to it because it does not depend on those particulars.

[agumonkey]

I'd even say that maths is what appears when you stop willing to pay for concretion.