I think a good, related example to your point is the “2 watched literals” algorithm used in SAT solvers. It uses lazy evaluation to significantly improve the speed of the SAT solver. I implemented an SAT solver a couple of years ago just for learning and when it came to refactoring my code to implement the 2 watched literal I had what felt like a moment of recognition of the cumulative time and effort of many people working in this field of research that it must have taken to arrive at this design. It’s just such an elegant implementation that to me seems it can only have come from deeply understanding the theory and implementation of SAT solvers.