Invariants: A Better Debugger?

I find the general point interesting, but want to nitpick:<p>&gt; &quot;items in the deleted state must have a deleted time&quot;<p>I much prefer making it impossible to represent bad state, like rephrasing at as &quot;items are deleted if their deleted_time property is set&quot;. In this case, that makes the deletion atomic: there&#x27;s never an instant where it&#x27;s ambiguous if the object was deleted.<p>That doesn&#x27;t disagree with his premise. It&#x27;s an additional recommendation.

Invariants are also an important part of Design by Contract [0], and more generally as class invariants [1] in OOP.<p>[0] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Design_by_contract" rel="nofollow noreferrer">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Design_by_contract</a><p>[1] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Class_invariant" rel="nofollow noreferrer">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Class_invariant</a>

&gt; Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician Tony Hoare, and subsequently refined by Hoare and other researchers.[1] The original ideas were seeded by the work of Robert W. Floyd, who had published a similar system[2] for flowcharts.<p><a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Hoare_logic" rel="nofollow noreferrer">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Hoare_logic</a>

I don&#x27;t think the two are comparable at all. Invariants are like tests or assertions, debugging deals with issues that are not handled well by either. You debug more when you invariant or test less, but one isn&#x27;t a replacement for the other. You can&#x27;t step through code or examine arbitrary registers with an invariant.

Invariants are for sanity. Debuggers are for when the invariants are found to have been violated.

I use assertions heavily in my own code and they work extremely well.<p>I don&#x27;t buy the distinction between assertions and invariants as made in the blog post though, as if one was a higher level variety of the other. You can assert anything (though it may get expensive!). I consider invariants to be the logical statement of what should be true, and an assertion to be a program statement that actually performs the check.<p>Terminology, terminology, it doesn&#x27;t matter. I agree with the author, it&#x27;s an incredibly valuable tool.

As an ABAP developer looking to get back into the normal world I&#x27;m a little scared about how debugging will be like.<p>After playing around with a bit of C and trying gdb, I asked myself if this is really what people use. The display constantly breaks and there&#x27;s not a lot of stuff to quickly walk through code and visualize what it&#x27;s doing.<p>If there&#x27;s something I don&#x27;t understand within 15 seconds in ABAP, I fire up the debugger.<p>ABAP is a ridiculously complicated language that&#x27;s been getting more and more features tacked on for 30 years and there are now about 1000 instructions in it. I firmly believe that there are some instructions in there that not a single person on earth understands, so it needs a good debugger to make it usable.<p>I jump into the debugger before even trying to look at the code because it shows me everything in the usual editor component and I can navigate through it as fast as I can read, so it&#x27;s basically assisted reading.<p>I couldn&#x27;t imagine doing anything like that with GDB. Am I just too stupid to go fast and quickly get information in GDB? Is there a better alternative that I completely missed. Is non-ABAP code just more abstract to a point where debugging in general doesn&#x27;t make much sense anymore?<p>Tying that back to the article: I agree that making all important assumptions explicit with assertions helps a lot with not shooting yourself in the foot. I can usually test the result and use my trusty debugger to find problems without assertions as well, but that requires remembering all my assumptions and knowing exactly what I want my code to do. If I write the assumptions down, I don&#x27;t have to remember them and the next dev will be able to see what I thought. I also don&#x27;t need to check if they still hold true since the runtime does that for me and hands a short dump to anyone who violates them.

In your experience, what properties makes a good invariant, and how does one find them in practice for a new system?

I think of unit tests and the debugger going together like peanut butter and jelly. That is, a language like Java lacks the interactive REPl of, say, Python but you can get similar interactivity writing tests in an IDE like IntelliJ Idea and breakpointing, and when you are done you wrote some tests.

I need to make better use of invariants.<p>Part of that is the brain damage from C where asserts disappear in release builds. This relegates them to second-class, despite the fact that it is trivial to write the equivalent with an if statement and an early return.<p>Swift’s guard keyword is really nice. We could really use Eiffel-style invariants in our PLs now, IMO.

Basic invariants are very helpful for developing data structures and algorithms if you can come up with good ones. The more the better, as long as they can be checked reasonably quickly.<p>For example, I was implementing a dynamic spatial data structure a while ago, so one of the first things I did is implement a validation function that checks the entire structure for consistency errors. Then as I implemented new features, I added calls to the validation after every change, and it caught way more bugs and edge cases than I expected. Easy to accidentally swap a &lt;= for a &lt;, and have it complete successfully, but produce subtly incorrect results that you&#x27;d never spot by hand.

&gt;&quot;Invariants, like assertions, are things that must be true during or after the execution of a piece of code. &quot;This array is sorted&quot;, &quot;the first item is the smallest&quot;, &quot;items in the deleted state must have a deleted time&quot;, that kind of thing. Invariants are broader than assertions: they can assert properties of a piece of data, properties of an entire data structure, or even properties of collections of data structures spread across multiple machines.&quot;<p>Yes!<p>In theory it would be possible to assert the correctness of an entire codebase with <i>only a single unit test(!)</i> ran on only a single piece of data(!) -- but that&#x27;s IF, <i>if and only if</i> -- the code is known to be tightly and invariably bound to that key piece of data such that its entire functionality can be asserted via the state of that piece of data!<p>There is a broader pattern here, too...<p>Let&#x27;s suppose we have a cup which is half-full, half-empty.<p>If we call the fullness of the cup &quot;X&quot; and the emptiness of the cup &quot;Y&quot; -- then if we know one of these things, one of these aspects of the underlying system -- then we also know the other one! (X&#x27;s relationship to Y is: X = 1&#x2F;Y, correspondingly, Y&#x27;s relationship to X is: Y=1&#x2F;X (inverse AKA reciprocal relationship...))<p>But the point is: <i>If you know the state of one, you also know the state of the other...</i><p>In the case of the theoretical codebase whose code is tightly, invariably, deterministically coupled to one key variable thus requiring only one unit test of that variable to assert the correctness of the entire codebase -- &quot;X&quot; is that variable, and &quot;Y&quot; is &quot;the codebase&quot;!<p>These relationships do not need to be inverse or reciprocal as with the half full, half empty cup of water example -- they can be <i>asymmetric</i>, as in the case of the theoretical codebase with the single unit test!<p>The broader broader pattern is &quot;if thing A (correctly and invariably!) asserts thing B -- then if you have thing A -- then <i>you also have thing B</i> (without needing to check thing B independently!)&quot;.<p>In Logic, this can be thought of as &quot;If A implies B, and you have A (A is True), then you also have B (B exists and is True -- as a result of merely having A)&quot;<p>In Business, one might compare the concept of KPI&#x27;s (Key Performance Indicators) to this -- if you have a KPI (measurement, observation) on the one hand, then you also have an asserted state of the business on the other, but remember, that&#x27;s <i>if and only if</i> the two things are tightly and invariably bound -- that is, aspects of the same underlying phenomena...