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.

> In the course of my work, I think of an invariant as a state that must hold true at all points during the software’s execution.

That seems quite close to the author's answer:

> Perhaps it’s time to answer the title question: invariant is some property which holds at all times during dynamic evolution of the system.

"Maybe a good analogy would be “a runtime assert”."

The first example if found when googling "python invariants" was a BankAccount class that did exactly this

class BankAccount:

    """ 

    A bank account class with a representation invariant: balance is always non-negative.

    """

    def __init__(self, initial_balance):

        self.balance = initial_balance

        assert self.balance >= 0, "Balance cannot be negative"



    def deposit(self, amount):

        assert amount > 0, "Deposit amount must be positive"

        self.balance += amount



    def withdraw(self, amount):

        assert amount > 0, "Withdrawal amount must be positive"

        assert self.balance >= amount, "Insufficient funds"

        self.balance -= amount

Why didn't Ada become as popular as Rust? I think I read that Ada compilers were incredibly expensive.