Assert(): A Modern How To
fiberfs.ioAn overlapping technique (covering some but not all of the circumstances you'd use assert) is to take a parse-dont-validate approach, and essentially encode the fact that an assertion has been applied to a value in its type.
How ergonomic this is will vary by language, but the general idea would be to apply the assertion logic in some sort of constructor, then prevent any operations which would break the invariant going forward. The simplest way to protect this being by making the value immutable where possible.
Users of the value who care about the invariant being true can then specify in their types that they want a non-empty-collection or a foo-id or whatever it may be, rather than asking for the wider type, then asserting.
It is so nice to come here and want to say something, and someone already said it.
For those who haven't read "Parse, Don't Validate": https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...
I'm not sure exactly what languages people think of when they consider asserting, but I presume it's Java, C# or C/C++. In Java asserts are disabled by default, so they're thought of as a debug/development utility.
In another thinkpiece, "It takes two to Contract", it is demonstrated how types and assertions work together in TigerBeetle: https://tigerbeetle.com/blog/2023-12-27-it-takes-two-to-cont...
I think people might be worried of asserting in production because "what if you hit an edge case in production that you haven't accounted for, and the system crashes?" And I either think "You just don't test enough", or "Parse, Don't Validate (rather than assert), report a problem and continue."
> Users of the value who care about the invariant being true can then specify in their types that they want
Now that C# has value types and Java has record classes, this kind of data modelling has become available in mainstream systems languages. I'm not a C++ shark, but I think the closest equivalent is C++20 aggregate structs.
Some of the newer Java features are really nice for this: sealed interfaces, records, sealed interfaces, and record pattern matching
Don't forget sealed interfaces!
I would say the killer features are records and pattern matching.
Sealed interfaces/classes seem to mostly compensate for hypermobility caused by inheritance (that you can modify a superclass'es behavior and break abstraction boundaries).
Stop relying on inheritance, and you don't really need sealed interfaces.
Using records and thus lowering mutable state makes the problem of breaking abstraction boundaries lesser as well.
This is a hot take paid for by the functional programming lobby.
I love to combine assertions with « restartability ».
If you’re program has entered an unknown, failed state, just restart it from a known state.
Even better if you can divide a complex system in sub modules that can recover independently without bringing down the entire system.
Something like Erlang supervision tree. Or at least a systemd Restart=always service.
if your program is mostly stateless, and « restartable », it becomes fault tolerant, and you can use assertions liberally and easily avoid unknown/bad states.
Invariants can be enforced, and correctness preserved. But an important question remains when an assertion is triggered, why invariants were violated?
We need to preserve context, and decide to handle or not this case. That is easy to forget in code that is assertions oriented.
> We need to preserve context, and decide to handle or not this case. That is easy to forget in code that is assertions oriented.
The old solution to that, which worked very well, was coredumps. The assertion fires and your program is taken down, but just before that we save out the entire memory area of your program. That way you can come in with a debugger later and poke around.
People would often leave some memory areas (typically circular buffers) with debug values that would be useful in debugging. They'd never be used anywhere in the program, unless the programmer had to poke around manually.
I've often wished this workflow was still considered high priority on modern runtimes.
You are very right. With linker maps, debug symbol files etc. we can get a good handle on what went wrong.
> People would often leave some memory areas (typically circular buffers) with debug values that would be useful in debugging. They'd never be used anywhere in the program, unless the programmer had to poke around manually.
In one Linux-based system i worked on, they had an area of memory between the heap and the stack where shared libraries are typically mapped in, sectioned off as a circular buffer via linker scripts for each module which was then used for all sorts of logging. A separate process would also map this memory area to provide a UI and also to write to disk. It was pretty neat and worked great.
> Can assertions be used in production?
Yes
> What should I be asserting on?
Invariants
> Can I customize how assert behaves?
It should abort the program, logging the stack and whatever the context you pass into in, printf-style. If it doesn't abort, it just buries the issue of the program being in incorrect internal state. It should never be OK.
I think part of the problem is that assert is used for different things.
You can use assert to cover a case that should never happen, you can also use assert to catch programming errors during development.
It's arguable that you don't want the second group in a production build. That should have been caught in testing.
But then there's the use where it's a lazy person's if statement. Instead of dealing with the issue assert it. I'm undecided whether this is a net good. Would the test have been implemented anyway?
Additionally recommended: if attached to a debugger, the program should stop in the debugger, immediately, without printing a message (you can look at the code), or getting a stack trace (the debugger can do that), or whatever else, to avoid possibly triggering further asserts or causing more problems. This leaves the state just as it was (or as near as feasible), so that it can be investigated.
After being stopped in this way, it must be possible to resume execution somehow. Asserts are code too, and they can be wrong, and it may not be clear why, or what the ramifications might actually be for the specific case - continuing to let the code run can be useful for debugging purposes.
The ASSERT (note caps) macro in Microsoft MFC library does this. It uses a "INT 3" instruction (x86/x64) via "AfxDebugBreak" to invoke the debugger.
Since the above is a well-known technique, it has now been generalized and standardized via "std::breakpoint" in C++26 - https://en.cppreference.com/cpp/utility/breakpoint
This function standardizes many similar existing facilities: __builtin_debugtrap from LLVM, DebugBreak() from Win32 API, __debugbreak Microsoft Specific C/C++ extension, debugger_break from boost.test, assert(false), _asm { int 3 } (MSVC) and asm("int3") (GCC/clang) for x86 targets, etc.
There's a whole big contentious point that the author completely ignored: using assertions in tests (like unit-tests). Some unit testing frameworks expect their users to use assertions to do the job, others are very much against it because they want to separate between the failures of the system under test from failures of the test. (If that matters, I'm in the later camp).
* * *
I also think that the article confuses the how assert works at present (in some languages. Obviously, not Prolog, for example :D), and how he wants it to work. Sometimes his reasoning for doing one thing or the other is based on how assert works today, and sometimes it's based on how he wishes for it to work. Both have merit, but put together don't make much sense.
As for me, I think that the bullet points the author gives for the "proper" use of assertions need to be covered by different tools. Especially if the program is to be compiled with optimizations. I don't think there can be a general rule to tell if an assertion should stay at runtime or not. Sometimes it will depend on the knowledge about the environment in which the program will run. So, you'd need "persistent assertions" and "transient assertions" for the lack of a better word, where "persistent assertion" is functionally an exception, it just checks the same thing as the "transient assertion" would, so it makes sense that they are both called "assertions".
> Some unit testing frameworks expect their users to use assertions to do the job, others are very much against it because they want to separate between the failures of the system under test from failures of the test. (If that matters, I'm in the later camp).
How useful is this distinction in practice? A failing test is going to examined in detail and that examination is going to reveal whether the system under test failed or if the test itself failed.
I guess I am asking, when is this distinction useful?
Oh... it's not just useful, people get red in the face and start swinging heavy object in the air when it comes to discussing this.
Imagine working in a larger company, where you routinely get close to a hundred of useless emails every day. Imagine they use some garbage mail server like the one provided by Office 365, so that filtering is broken, emails get lost all the time etc. And now your CI is sending you alerts about code breakage, and you need to... wait, not just scroll through an endless Jenkins log, you need to download, unzip the artifacts, figure out which files are the test logs, and from there try to figure out what the test was doing and whether the error has anything to do with your code.
This whole process is infuriatingly unnecessary, tedious, it contributes nothing to whatever goals you've set for yourself. It's a toil that you have to engage in every day, perhaps for hours, just to come back with the answer "looks like it's not my problem after all".
I know this because I've been on the receiving end of this anger and frustration :) And I've never found a good way to eliminate this problem completely, but I'm sure that narrowing down the number of people the problem is reported to only to the most relevant people helps.
A typical place this distinction is useful is that it determines whether the test-suite runs to completion with multiple tests, or panics/terminates hard on the first failure.
Not this again ...
Assertions should only be thought of as predicates on state space to ensure program correctness. Everything else is just a corollary.
Some relevant past comments of mine here - https://news.ycombinator.com/item?id=48358691
If you say so it must be law
Ha, Ha ...
I have pointed to previous discussions with other HN users where the logic and rationale behind my "say so" are given. If you actually cared to read them you will find quite long back-and-forth on formal methods and a whole lot of references for edification.
It’s interesting that the author lands on an API much like the function signature for TAP (Test Anything Protocol).
ok( conditional, message );
Personally I'm not much of a fan of assert()'s... at least in the language I use the most (C++). It's not that I don't think you should validate the input ranges of parameters to functions its that in general exceptions are better.
The article gets things flatly wrong from its first, ah, assertion. Asserts aren't for validation: the condition is supposed to be impossible to be false, just not provable by the type system. If invalid input can come through normal operation of the program, you use a normal runtime check, not an assert.
> Asserts ... the condition is supposed to be impossible to be false, just not provable by the type system
Very nicely said!
If we're trying to outline a future for assertions, I think it would help to situate them among the other mechanisms we have for ensuring correctness and explain where assertions have the right tradeoffs. For example, what unique need does a production assertion API satisfy that a normal conditional throw does not? Are there cases where production assertions are still necessary even when invariants are established through type constructors?
Asserts are a goto of ensuring correctness. Versatile, powerful, and incredibly easy to misuse.
Whatever correctness goal you're trying to achieve, there are safer, more ergonomic, and stronger alternatives you can reach for: type systems, contract systems, and even normal exception handling are often better. However, if you work in a domain where such tools can't be used or are not available, assert will still be there for you. It's worth knowing how to use it for that situation, but you should favor less ad hoc, more systematic features to ensure correctness in day-to-day programming.
> For example, what unique need does a production assertion API satisfy that a normal conditional throw does not?
See https://news.ycombinator.com/item?id=49231133 An "assert" is for "impossible to fail" conditions while "throw" is for conditions which might fail within the valid state space of the program.
> Are there cases where production assertions are still necessary even when invariants are established through type constructors?
Yes. Even though there is an equivalence between "Predicates <-> Types" (Curry-Howard correspondence) many languages do not have a robust type system to avail of this (eg. C). In the "Axiomatic" approach to "Programming Language Semantics" a language construct's (eg. if/switch/while etc.) specification is given by "precondition and postcondition" which are asserts that must hold before and after the construct. This is the famous "Hoare Triple" and later extended by Dijkstra in his wp-calculus and demonstrated in his "Guarded Command Language". The same idea holds when the code between precondition and postcondition is a function/class/module/etc. in which case it is called a "Contract" for that piece of code.
Interesting article about a worthy topic, even though I disagree with some it. Side note: I expected to see mention of design by contract and function preconditions/invariants/postconditions.
I don't think the article is well founded. Before you can discuss usage you need to establish the semantics for assert(). The author touches on this in the introduction but then leaves the details unexamined. In particular I'd need to know: can assertions be disabled (as with C/C++ NDEBUG)? does the project have a policy of leaving asserts in production builds? or are asserts only ever enabled for development and testing. if used in production, do you care about the overhead of checking assertions in performance critical code? if an assertion is hit does it always log and panic/terminate? or does it throw a catchable exception? What is the runtime context of the code: is it a server process with a supervision tree? is the failure paradigm "let it crash"? is it an interactive program where the only supervisor is the user? is it a use-case where a program crash is undesirable and/or safety critical? is it a library with unknown use-cases? Are the developers in full control of the program inputs and outputs that trigger asserts?
As a general principle for layered systems, when there is a policy decision to be made, lower-level code should delegate upwards to higher levels, which should implement the policy. Throwing an exception or returning an error code is frequently better than terminating (if you squint, crashing out to the supervision tree is more like throwing an exception than it is like terminating.)
> Correctness - All possible function input and output values which do not have full value coverage should have assertions covering them.
Only if you control all of the callers. Library users would prefer an invalid parameters error/exception.
> Safety - When performing operations that can have unwanted, known, or unknown side effects, assertions should be used to prevent those conditions from happening.
Why assertions? If it is safety critical, shouldn't these checks be mandatory?
> Development - Use an assertion to enforce assumptions on values and state. These assertions can optionally be compiled out of code when coupled with proper testing.
This is where preconditions/postconditions/invariants come in. If safety is important you probably want to leave them in place. A runtime contract violation should enter a fail-safe state.
> Documentation - When writing code, use assertions as self documenting guardrails around your logic. Use assertions to enforce values and state which might be unclear from documentation or hard to decipher from reading code.
I do this, but in this case you either need to be 100% sure that the exception won't get hit, 100% sure that the exception won't make it into production builds, or okay with production crashes.
> var error = system_call(...);
> assert(!error);
> Side note: I expected to see mention of design by contract and function preconditions/invariants/postconditions.
For some reason, DbC seems to be virtually unknown to most programmers. It's incredibly strange: I was sure that DbC would be the next big step after gradual typing. It's just such a natural fit: where the type system gives up (any/dynamic), the contract system can step in. There are papers on automatically generating contracts from types (and vice versa) to allow typed values to flow through untyped code; there are papers showing how to make that performant enough; papers showing how to instrument systems to generate types and contracts from tests; etc. They are all 15-20 years old now, yet there's still nothing suggesting that the mainstream even looks that way, much less actually implements something usable.
Can you share the links to all the papers that you refer to?
The ones I most likely had in mind (recovered with help from ChatGPT due to my memory being fuzzy - but most links it produced were in my bookmarks):
- Matthias Felleisen, Sam Tobin-Hochstadt, “Interlanguage Migration: From Scripts to Programs” (DLS 2006)
- Sam Tobin-Hochstadt, Matthias Felleisen, “The Design and Implementation of Typed Scheme” (POPL 2008)
- Sam Tobin-Hochstadt, “Typed Scheme: From Scripts to Programs” (2010).
- Asumu Takikawa et al., “Gradual Typing for First-Class Classes” (OOPSLA 2012)
- Esteban Allende, Johan Fabry, Éric Tanter, “Cast Insertion Strategies for Gradually-Typed Objects” (DLS 2013)
- Esteban Allende, Johan Fabry, Ronald Garcia, Éric Tanter, “Confined Gradual Typing” (OOPSLA 2014).
- Nadia Polikarpova, Ilinca Ciupa, Bertrand Meyer, “A Comparative Study of Programmer-Written and Automatically Inferred Contracts” (ISSTA 2009).
There's a lot more research and literature on the topic. Naive approaches were tried ~2010 and were shown to be performance disasters, but by ~2015 we already had those issues mostly solved. I seriously thought that every new language (or new release of an existing PL) after that would feature first-class support for contracts and gradual typing, along with built-in support for automatically generating/harvesting types and contracts from tests. It's 2026, and the mainstream still doesn't seem aware of the possibilities, much less actively going in that direction. It's nuts!
Thank You and Appreciate it very much!
The 1st, 4th and 7th papers look especially interesting.
I think in order to appreciate DbC (gradual typing is whole another beast altogether) one needs to have some idea of "Program Correctness" concepts in the lineage of Floyd/Hoare/Dijkstra and Meyer. With LLMs it is even more important to use the above as a "Correctness-by-Construction" (CbC) approach to code generation. To me this is the need of the hour and yet i don't see people talking about it;
Correctness-by-Construction (CbC) - https://www.tu-braunschweig.de/en/isf/research/cbc
Correctness-by-Construction: An Overview of the CorC Ecosystem by Bordis, Runge et al. - https://dl.acm.org/doi/10.1145/3591335.3591343
The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - https://link.springer.com/book/10.1007/978-3-642-27919-5
> I think in order to appreciate DbC [...] one needs to have some idea of "Program Correctness" concepts in the lineage of Floyd/Hoare/Dijkstra and Meyer.
Agreed. To me, full-program (or system) formal verification is something I'd love to have, but I also acknowledge that even champions of formal methods (like Tony Hoare you mentioned) doubt its practicality, due to how large our software systems tend to be nowadays. If so, then let's take as much as we can from those methods (powerful, expressive type systems) and let's complement that with proper infrastructure for ensuring correctness (contracts, invariants, various kinds of automated tests) that are weaker, but much more applicable in practice.
Unfortunately, we're still stuck in a place where a plain `assert` - basically a "goto of ensuring correctness" - needs to be introduced to people with posts like the OP's...
> To me this is the need of the hour and yet i don't see people talking about it
Yes, I feel the same. I think the reason here is that we (programmers, collectively) didn't really take correctness of our programs seriously before, so there's just not much awareness about the research and work done in this problem space. Many people now are ready to admit that yes, we do need stronger, more comprehensive and better integrated tools for controlling, showing, and ensuring correctness - but the need for them arrived so quickly (and along with so many other, serious changes to the craft), that they simply haven't been able to catch up on the prior work fast enough. It'll probably take a few years, at least, for the urgent need for better tools to become widely recognized. It'll take even more time to get to usable implementations.
> (gradual typing is whole another beast altogether)
It's actually not. Contracts in Racket are duals of types (well, not fully, since you can put arbitrary code in a predicate and make that into a contract; however, that's more of an escape hatch than the default use of contracts in Racket). Typed Racket can wrap a typed value in a contract that guarantees that, when the value comes back, it exactly conforms to its type. This way, you can avoid expensive casts. Moreover, Typed Racket has refinement types (ie. that a given int will always be greater than 0), and these refinements have direct contract equivalents, too. So a Typed Racket value can be statically proven to have that property on the typed side, and then you don't have to check or prove it again when it comes back from the untyped world.
I believe this is an extremely neat capability that ties types and contracts together, opening some very interesting possibilities. Like, if a contract can be expressed as a refinement on a type, and we already have support for that in the type checker, we can automatically promote such contracts into types! That's huge, because if the contracted value never leaves a well-typed environment, we can eliminate all runtime checks without affecting correctness. It also addresses the most common problem with contracts (and assertions): runtime overhead.
I'm aware of all that because I decided to build an environment that would blend a fast, interactive development loop, an isolated environment in which agents can comfortably live, and an expansive toolkit for checking and ensuring correctness. I'm building it on top of Pharo Smalltalk, Glamorous Toolkit, and an extended Gradualtalk implementation that would also handle contracts. There are some problematic parts, but if I manage to achieve my goals in a Smalltalk image, I feel like it'll prove it can be achieved in literally every other environment, too :)
EDIT: Forgot to mention, there's a pretty extensive list of papers on contracts and gradual typing here: https://samth.github.io/gradual-typing-bib
EDIT: "Types to contracts" is already presented in papers I referenced before (Typed Racket ones); forgot to mention the "contracts to types" (or rather, static verification of contracts) part: "Soft Contract Verification for Higher-Order Stateful Programs" and "Soft Contract Verification" by Phuc C. Nguyen et al.
Nice.
I should have inferred that you were talking about Racket since some of the papers you had listed were Scheme related. Gradual Typing and similar powerful type systems are not available in the world of C/C++ where i come from (though modern C++ has a few simpler similar features). Hence my comment on that.
We already know from Curry-Howard isomorphism that "Predicates (i.e. Contracts) <-> Types". It is actually easier to first think of only predicates over the state space which can then be mapped into a type. Here you think of types as sets (as a first approximation) and predicates establishing a relation(a set of tuples) over a subset of their cartesian product. The logic is explicit with no unnecessary abstractions obscuring the concepts. This was Dijkstra's approach which is at the heart of CbC and important for us to understand.
If you straight away start with type systems with a "standard" programmer they are lost. The mistake we do is that we do not properly show the mapping of discrete mathematics onto the constructs of a programming language. With FP languages the problem is compounded since it is based on lambda calculus and so the idea of a type is even more generalized in a different dimension.
IMO, with LLMs generating gobs of code now, we need this in some form yesterday. CbC gives you one approach where the specifications are Predicates (invariants/contracts/etc.) which is successively refined to get the final program but preserving correctness at every step.
Your project sounds quite interesting; Good luck with that! You might want to write a paper/article on that for wider dissemination.