Invariants: A Better Debugger?
brooker.co.za
brooker.co.za
> "items in the deleted state must have a deleted time"
I much prefer making it impossible to represent bad state, like rephrasing at as "items are deleted if their deleted_time property is set". In this case, that makes the deletion atomic: there's never an instant where it's ambiguous if the object was deleted.
That doesn't disagree with his premise. It's an additional recommendation.
In such cases I fall back to computed columns. A deleted flag which value depends on deleted_time being set or not, for example. This retains your atomic state goal.
That said, Zig does make it pretty easy to handle a lot of the features you might want. As a library, you can offer the ability for a person to rewrite a type (maybe only in non-optimized modes if you want) and check the invariants before/after every public function call. You can always add explicit pre/post-condition checks to any function you'd like. Invariants in your inputs/outputs can be hoisted to the type checker (I wrote a toy project doing this [0]). Like...at some point you have to describe what you want to check and when you want it to run for the invariant checking to be useful, and Zig allows you to write the checks and use comptime magic to place them where you want them to run, all in the userspace of the language. Which language features would you like to make the process smoother (automatic subtype resolution on a lattice of constraints, a bit of syntax, ...)?
I try to code small, assertion-like "invariants" into my programs via guard clauses and... assertions. When I get an error, it's usually handled by those, so I pop open the debugger, break on the exception and trace the stack back to see where I should have had a higher-level assertion or guard clause.
Invariants to make debugging fast and easy (and to force me to write better code in early, malleable stages), debugger to show me exactly where I wasn't thinking it through.
I don'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.
Terminology, terminology, it doesn't matter. I agree with the author, it's an incredibly valuable tool.
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's not a lot of stuff to quickly walk through code and visualize what it's doing.
If there's something I don't understand within 15 seconds in ABAP, I fire up the debugger.
ABAP is a ridiculously complicated language that'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.
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's basically assisted reading.
I couldn'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't make much sense anymore?
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't have to remember them and the next dev will be able to see what I thought. I also don'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.
gdb has a tui that can show you multiple panes of information at a time, e.g. the source code, disassembly, and registers.
Other tools like Emacs, Eclipse, and CLion can use gdb as a backend and provide a friendlier interface on top.
It’s basically saying: “It’s great software, once you finish writing it yourself.”
But I'm an emacs user so obviously that fits my psychology :)
Here's an example of modern tools:
https://twitter.com/EskilSteenberg/status/169533726869157102...
That so far has been my frustration when not remote debugging linux vm, where it becomes a gdb front-end
Watched the video and you pretty much have everything mentioned in it with just an lsp, compiler flags and a command that runs your program with a debugger. The only example that wasn't caught with just that was the p[3] example but that was caught by valgrind which is also something I have a command setup for.
Really the only thing I was actually jealous of was at the very end of the video and it wasn't the hot reloading stuff, that's easy if you split your programs from the platform its running on. The ONLY thing was that the vs debugger lets you explore variables with a visual interface instead of having to write commands to do it. I've used it on windows and even though its usually busted and variables do not always update they sometimes do. At the very least just viewing the hiearchy of the structure is useful so that you can easily add the value you want to the watch window which usually does work.
lldb does work on Linux.
As someone doing programming on unix since 2001, hell no, that's not what I use (directly), for the reasons you say.
I mean gdb in the backend is okay. And gdb actually specifies Gdb/MI, a protocol to remote-control it.
You can also use gdb directly locally this way, and then it sucks less.
But nowadays I just use the IntelliJ IDEA IDE. I wrote https://github.com/daym/idea-native2-debugger which is a native debugger plugin (that uses gdb in the back) for IntelliJ IDEA Community Edition. You can also use CLion (requires you to subscribe--but it's totally awesome and has a lot more features) and that uses lldb in the back instead of gdb.
Some of my friends use emacs with gdb debug thing. Seems to work OK too.
Earlier in life I used https://www.gnu.org/software/ddd/ a lot--but nowadays I just stay in IDEA.
After you got used to IDEA, using anything else is like riding a kick-scooter after you got used to a motorcycle.
emacs is also good as an IDE--but for me it just doesn't work well enough--and I'm not interested in having to maintain my editor configuration like an extra software project.
You can also extend gdb with python plugins that make your variable printout nicer and/or more complete. It's very good.
Can't read from a closed file? Assert the file is open.
The classic, transferring cash from account a to account b? Assert that a+b before = a+b after.
Object should be in a given state after a certain method is invoked? Assert it.
It is possible to assert some invariants at compile time using strong typing, that's pretty useful too and I'm learning to do that myself (nothing clever, it's just thinking of 2 different classes to represent 2 different states, or use phantom types). More complex compile-time assertions are possible using dependent types, but that's out of my pay grade at the moment.
Edit: assertions can come before and/or after the thing is done. Technically if you're checking before then it's a pre-condition you want to ensure, if it's after, then it's a post-condition check you're doing. Let's take the square root example, and assume that you're actually implementing a sqrt function, not just calling a library function. The pre-condition is as before, that f must be positive, and the post-condition is that for the result r, r*r = f (if you've successfully taken the square root of a thing, squaring it should get you back to the original value, or at least very, very close). HTH
As for taking as invariants anything that must be true, in a system very many things are true, and the most part of them would be utterly uninteresting. Understanding the process that one would use to pick insightful ones is rather the art which I'm intrigued by.
And which are you more likely to be writing, a distributed garbage collector or a single-core library/application? Realistically, very much the latter. And if the former, much of that system will be made up of stuff running strictly on single cores, to which plain bog-standard assertions will be just as useful.
> one would use to pick insightful ones is rather the art which I'm intrigued by.
Well, it's not really an art, it's more straightforward than that (edit: think of them as basic sanity checks, not anything deep or profound), but if my overview of the idea isn't helpful you need to provide a more concrete example to discuss. I think your question as it stands is too ill-defined.
[1] Edit: no, a postcondition expresses an invariant in code - but that's a terminology thing. We may be disagreeing just on terminology here.
postcondition is something which must be true after some code executes
invariant is both: something which must be true both before and after some code executes.
So it's the other way around. An invariant is a postcondition, but a postcondition is not necessarily an invariant.
(you can check all three with assertions, but they will generally exist whether you check them or not)
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.
Swift’s guard keyword is really nice. We could really use Eiffel-style invariants in our PLs now, IMO.
See e.g. https://dafny.org
Among other things you probably DO want to get rid of them when doing coverage analysis-- unless you like seeing your code base that truly has 100% branch coverage report as only having 30% coverage due to all the invariant checks that can't be triggered because the code isn't buggy.
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 <= for a <, and have it complete successfully, but produce subtly incorrect results that you'd never spot by hand.
Yes!
In theory it would be possible to assert the correctness of an entire codebase with only a single unit test(!) ran on only a single piece of data(!) -- but that's IF, if and only if -- 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!
There is a broader pattern here, too...
Let's suppose we have a cup which is half-full, half-empty.
If we call the fullness of the cup "X" and the emptiness of the cup "Y" -- then if we know one of these things, one of these aspects of the underlying system -- then we also know the other one! (X's relationship to Y is: X = 1/Y, correspondingly, Y's relationship to X is: Y=1/X (inverse AKA reciprocal relationship...))
But the point is: If you know the state of one, you also know the state of the other...
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 -- "X" is that variable, and "Y" is "the codebase"!
These relationships do not need to be inverse or reciprocal as with the half full, half empty cup of water example -- they can be asymmetric, as in the case of the theoretical codebase with the single unit test!
The broader broader pattern is "if thing A (correctly and invariably!) asserts thing B -- then if you have thing A -- then you also have thing B (without needing to check thing B independently!)".
In Logic, this can be thought of as "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)"
In Business, one might compare the concept of KPI'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's if and only if the two things are tightly and invariably bound -- that is, aspects of the same underlying phenomena...