One of the challenges of teaching higher education is that a lot of folks have a lot of opinions about what students should know. This is particularly true in engineering where students could end up working literally anywhere. As a result, how do you know what they should know? Well, that’s a question for a different time, but I do know what they don’t need to know: loop invariants. Come along with me on my beautiful rant about one of the most useless topics taught in computer science education.

## My Gripe With Loop Invariants (And Beyond)

As an educator in computer science, I often find that we teach students topics that they’re never going to use. In general, I’m not against the idea of learning for the sake of learning. However, until college is free for everyone, we really need to be focusing our programs on utility. And nowhere is this happening less than in computer science programs, which fixate heavily on high-level math abilities.

Don’t believe me? In an introductory programming course I teach right now, we cover topics like loop invariants, cryptography, mathematical modeling, number systems, and Monte Carlo estimation. As students move through most CS programs, they’ll also have to learn various forms of calculus and algebra. In most cases, they’ll even have to brush up on their formal logic and proofs.

Again, I don’t think any of this is actually bad. For instance, knowing how to prove things can improve your ability to create arguments and provide evidence—both important real-world skills. Likewise, familiarizing yourself with formal logic can help you generate better code.

However, when math is used as a tool to gatekeep people from the field, it can often feel a bit ridiculous. After all, how much math does a web developer really need? What about folks who work in IT or finance? Surely, basic math is enough. And if it’s not, we should be better educating students on what they actually need to know for the specific subdisciplines they’re interested in, right? You want to do machine learning? You better learn some statistics. Interested in graphics or game development? You might want to pick up some linear algebra.

My personal gripe is with the general obsession with proofs-based algorithms courses, an area in which I personally struggled a lot. In fact, I failed my first qualifying exam based solely on the algorithms portion of the exam. Yet, I seem to be doing fine in the field.

All of this brings me to the topic of loop invariants, which is a subject I actually teach students. Recently, I told my students that I would be willing to bet them money that they would never have to write their own loop invariant. Ever. While somewhat joking, I wondered just how much loop invariants are actually used. I never used them in my short engineering career, and I never learned about them in my undergraduate or graduate education. So, who’s actually using them? That’s what I sought to figure out today.

Having never once used a loop invariant, at least in the formal sense, I needed to know if this was a widespread trend. I figured one way to do that would be to look at the general interest in the topic through the lens of a massive search engine, Google. To do that, I dropped the phrase “loop invariant” right into Google Trends, which produced the following plot:

As stated by Google itself, interest over time is defined as follows:

Numbers represent search interest relative to the highest point on the chart for the given region and time. A value of 100 is the peak popularity for the term. A value of 50 means that the term is half as popular. A score of 0 means there was not enough data for this term.

In this case, the term “loop invariant” was most popular in October of 2004. On average, however, loop invariants sit around a 6 on the 100-point scale. Unfortunately, this doesn’t really tell us a lot. Perhaps, the term was extremely popular at point and hasn’t reached that level of prominence since. As a result, we have to compare the term to other terms in the space. To start, I decided to compare to another term that I see used a lot in academic spaces but not so much in practice, design by contract. Let’s see how it compares:

Okay, so design by contract follows an almost identical trend. It was a popular search term in the early 2000s, but folks haven’t really searched for it since 2010. Though, there does seem to be a slight uptick in the topic as of last month (March 2023). Maybe that’s my fault.

On the flip side, what about software development terms that we all know are used in practice, such as version control? Let’s see how that compares:

Okay, yikes! It’s not particularly close. It seems in general that software development terminology has trailed off since the beginning of Google, but version control is of significantly more interest than topics like design by contract and loop invariants. On top of that, I find it funny that even when loop invariants were popular, they were still way less popular than version control. Overall, that makes sense given the difference in utility, but it’s funny to me regardless.

At this point, I am sold on the idea that no one uses loop invariants, but I figure I ought to toss in a few more terms. Up next, continuous integration:

In general, I figured continuous integration was a more recent development in the field, but it’s still not particularly close. What about unit testing?

Well, that’s even worse! How about a topic that’s both popular in academics and applicable to the job, like data structures? Here’s the damage:

And for fun, here’s a comparison of a handful of terms on the course schedule for my students:

And another one to make y’all really sad:

I find this plot particularly funny because we teach both XML and RSS, and I think they’ve both fallen off pretty hard. However, they both still have more utility than loop invariants. Here’s another plot showing XML’s competition, JSON:

As you can see, it’s not quite to the level of search volume as XML was initially. However, it holds a major share of it today. Regardless, let’s get back to the point.

While Google Trends is a great tool for seeing what folks are searching for, I think it’s also helpful to look at what folks are actually writing. In other words, what are people saying in terms of the utility of loop invariants? Not just that, but when is the last time anyone wrote anything about loop invariants? It’s perhaps not surprising what I found.

To start, I tried searching “who is using loop invariants?” to no luck (though, should I really be surprised?). Off the top of the search index, we see:

1. Loop Invariant Condition with Examples by Geeks for Geeks
2. Loop Invariant by Wikipedia
3. What Is a Loop Invariant? by Baeldung
4. What Is a Loop Invariant? on StackOverflow
5. Loop Invariants Can Give Your Code Superpowers by YourBasic
6. Loop Invariant Proofs by Eindhoven University of Technology
7. Loop Invariants by University of Miami.

And, it keeps going like that. Most of the links following are from universities with generic loop invariant pages. As a result, I had to do a bit more work. For instance, I noticed a series of related questions under the StackOverflow link. One in particular read: “Opinion on ‘loop invariants’, and are these frequently used in industry?‘ I’ll let you guess the year it was posted (hint: 13 years ago). And by the time I got to it, it only had 996 views.

If you read through that thread, you’ll find that the comments are filled with the traditional snobbery. Unfortunately, the question isn’t really answered in the way it’s framed in the title. Most folks address the idea of the utility of proofs, which I think is a different question than “are loop invariants used in practice?”

As a result, I figured I’d modify my search query to read “loop invariants useless.” And wouldn’t you believe it? The thread I linked above was the second search result. The first, however, was a similar thread on Reddit titled, “Are Loop Invariants Ever Actually Used in the Real World?“, which was written much more recently (hint: 11 years ago).

The sentiment expressed by the author of the post almost sounds like it could have been written by one of my students. They state:

I’m in a Data Structures course at a community college and the instructor told us “In my entire career I’ve never seen anyone perform a loop invariant test… but we’re going to learn them anyway”… These seem like the most useless things in the world..

FerretWithASpork, 2012

Clearly the internet was a different beast back then because the comments are filled with similar snobbery. For instance, the top comment uses that weird English phrasing where the word “one” can act as a pronoun (e.g., one must never…). In their exact words, they argue for the benefit of loop invariants by stating, “I’m of the opinion that one should understand what one is coding.” Like I get what they’re saying, but it sure feels like they care less about loop invariants and more about excluding folks from the field.

On the flip side, I did notice a few reasonable takes, such as this one:

From what I’ve seen and read they’re more common in areas that are really pushing the boundaries of what we know how to do than in more routine programming. Most programmers never use them, but I’ve met a guy who works in AI R&D who likes to use them for his every day work, but I think he’s in the minority.

When it comes to education, they’re valuable in the same way proofs are in math – they force clear thinking.

Sklargblar, 2012

Overall, I didn’t really see anyone claiming loop invariants were used regularly. Instead, most folks either agreed they weren’t used or took time to mock the original poster. The closest I got to an answer was from this post:

It depends on how you define ‘the real world’.

Is academia included in the real world? Is algorithm engineering and theoretical computer science part of the real world? We have used loop invariants in every algorithms course and some other courses as well at my university. Sometimes they are implicit .. the book does not say ‘we use a loop-invariant to show that … ‘ but it is still part of the correctness proof of most algorithms.

They are the CS equivalent of proofs by induction. Do you ever see proofs of induction in the real world? Maybe not so often in industry, but it is still a fundamental part of understanding what it means for something to be correct!

Lintheru, 2012

Which again, I found a bit too harsh for my liking. Clearly, this fellow was upset by the use of “real world,” which I think can be reasonably interpreted as “the norm” or “on average.” Academia, algorithm engineering, and theoretical computer science must all be incredibly small pieces of the broader programming community. So, ultimately, I’m still skeptical of the actual utility of loop invariants.

## The Verdict

All of this is to say that while I don’t think loop invariants have a place in broader computer science education, excluding specialized courses, I’m one of the few who have actually tried to argue for their benefit. Back when I was writing about the issue with using flags in code, I wrote about the role loop invariants can play in writing better code:

That said, people in general don’t write loop invariants, so who cares? Well, loop invariants force us to write explicit loop conditions which actually leads to better formed loops. I know the logic is somewhat circular, but the idea that the loop condition and loop body are separated follows a broader best practice: decoupling.