but a very large fraction are unaware of the formal definition

I think far too much is made about "formal definitions". Back when I did my formal CS education, I chose a multi-part long questionon big-O as my optional question. I passed the exam with distinction. Of course they don't tell you anything more than the overall scores, but I think I would probably have had to have scored perfectly on the four compulsuries to achieve that if I'd totally flunked the optional. Back then I could have, and probably did, give a formal definition of big-O and big Omega.

But over a 25 year career, I never once needed to repeat it. And nor has it ever been useful to me. But the education means that I do have a way of informally discussing algortihmic complexity in terms that many other programmers recognise and understand. So in that sense the knowledge of it is useful.

But in the real-world, when, as you point out, an O(n^2) algorithm in one language can out perform an O(n log n) in another; when memory allocation/reallocation costs can render a formally faster algorithm slower than a formally slower algorithm, because the latter is more cache friendly (eg. Mergesort versus QuickSort); and given multi-tasking OSs and mutli-core hardware renders static formal analysis iffy at best and an outright lie at worst; the usefulness of big-O is pretty much limited to discussion purposes only. A benchmark run many times under real-world or realistic conditions renders it mostly redundant.

A starting point, and a means of informal discussion, but little more.