Comment by mkl

Binary search is a very old trick, going back to 1946 on computers, and probably thousands of years before that, since searching sorted lists goes back to at least ancient Babylon. https://en.wikipedia.org/wiki/Binary_search