How can a binary search be written correctly?

In the discussion of the article Only 10% of programmers are able to write a binary search so no one has written how to properly approach the solution of this problem.
If we do not want to use the cyclic method “fortune telling, then testing, then correcting errors,” then we cannot do without the cycle invariant.
A loop invariant is a relationship that is true before the cycle, true during the execution of the cycle, and true at the exit of the cycle. All this is described in Dijkstra’s book “Programming Discipline”, and chewed up in detail in Gris’s book “Programming Science”. However, according to my observations, in practice this method is practically NOT used by anyone, considering that all this has nothing to do with reality. This is a big mistake.

Bentley himself c. 51 results in the following invariant: “if the element T is in general in the array X [1..N], then it must be in some area belonging to X”. Initially this area is the entire array.
This formulation is rather slurred. I think the reason for this is that Bentley has little experience - he, like many, uses this whole theory only for learning, and not for real life.
When I read the book of Bentley (long ago) and came to the words “So that you believe it - put this book aside right now and try to write the program yourself” - I covered the book and rather quickly found a normal wording.
We define the region O along the edges of the array so that it does not contain the required element T. This will be the cycle invariant: “the required element T is not in the region O”.
Initially, this area consists of two non-adjacent pieces of zero length (thickness, if you like) at the beginning and at the end of the array. It does not contain the required element, since it is empty and contains nothing at all.
If in the process of work this area covers the entire array, then there is no required element in the array.

Formal notation (letters and array dimension 1..N as in Bentley):
Aj: 1 <= j <L or U <j <= N: X [j]! = T
Originally L = 1, U = N, the area is empty.
When will the area cover the entire array? When L> U, you can draw and check the cells. This condition will be used to exit the loop.

Now about the contents of the cycle. Suppose the middle element (we denote its index as M) of the array X is not equal to the desired element T. How can we change L and U so that the invariant remains true? In this formulation, the task is so simple that there is no place to be mistaken. If T is greater than the middle element, then there is no T in the entire piece from 1 to the middle element. Similarly, if T is less than the middle element, then the entire piece from the middle element to N does not have T. The region expands, in the first case L: = M + 1 , in the second U: = M-1.
')
Note that all the main points of the algorithm, namely: the condition “L> U” for exiting the cycle (negating “L <= U” for continuing), changing the boundaries of the area L: = M + 1, U: = M- 1 we did not derive fortune telling, but by strict, with very simple reasoning.

Here is the resulting algorithm in pseudocode:

 L: = 1;  U: = N;  found: = false; 
 while (L <= U) & not found do 
   M: = midpoint of the segment L..U; 
   if a [M] = T then
     found: = true;
   elseif a [M] <T then
     L: = M + 1;
   else
     U: = M-1;
   end;
 end