CLRS defines loop invariants pretty clearly: We must show three things about a loop invariant: Initialization: It is true prior to the first iteration

CLRS defines loop invariants pretty clearly: We must show three things about a loop invariant: Initialization: It is true prior to the first iteration of the loop. Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration. Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct. Which is very much what the article says: lo <= insertion_point <= hi should hold on every iteration. It clearly holds before we enter the loop. [...] The invariant, the condition binding lo and hi, holds on every iteration. They are indeed observable and testable during runtime, but beyond just being dependencies on certain subsets of your state space, or "runtime asserts," they are properties that must hold as a necessary consequence of the operation of the algorithm. One proves that an invariant is necessarily true in the process of demonstrating the correctness of an algorithm. In terms of concrete implementations of an algorithm, this in some way makes the "runtime assert" redundant, for, at least in principle, one can statically analyze the code and then prove, before runtime, that the expressions being asserted must necessarily be true (subject to certain preconditions), and even optimize them out. Of course, this presumes that you have indeed implemented the algorithm correctly - and one way to determine this is to see whether or not your implementation satisfies those same properties and invariants that the abstract description of the algorithm depends upon, and the article also discusses this point.