Asserts in Zig(kristoff.it)
kristoff.it
Asserts in Zig
https://kristoff.it/blog/fix-your-asserts/
20 comments
To add on to this, the C++ proposal for [[assume]] [0] came to a similar conclusion and cites MSVC's experience with an assert-in-debug-assume-in-release construction (i.e., removing the assumptions resulted in a 1-2% speedup and increased reliability) as a reason to not tie assertions to assumptions.
[0]: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p17...
[1]: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p20...
[0]: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2022/p17...
[1]: https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2020/p20...
I recently worked for a company with a large C++ codebase. For many years they relied entirely on asserts in QA builds to catch errors, no unit testing or production asserts. When I joined about three years ago they had just started to pick up unit testing, and would be enabling asserts in production “soon” (once all the most common ones had been fixed).
I left a little over a month ago, and the status on that was still “soon”. Some bad practices early on are just really hard to dig yourself out of.
I left a little over a month ago, and the status on that was still “soon”. Some bad practices early on are just really hard to dig yourself out of.
I believe this is just about the behavior of std.debug.assert.
You can pretty easily have a different kind of assert that disappears in release builds (if you want).
You can pretty easily have a different kind of assert that disappears in release builds (if you want).
It's in the article.
> you can implement your own version that internally checks a build-time flag, approximating C/C++ behavior
> you can implement your own version that internally checks a build-time flag, approximating C/C++ behavior
I really like the Oracle tutorial on Java asserts.
https://docs.oracle.com/javase/8/docs/technotes/guides/langu...
And I'm pretty happy with its design considering its age.
Notably this is not a function call and indeed things are not called unless you enable it. Contrast with Zig. So I guess you will only suffer from code bloat if you never enable them.
The tutorial mentions the dangers of side effects. But it also mentions how to use them for more complicated assertions. That's natural since you'll want something like that when you need to check a post-condition.
Programming assertions get joked on because of, ahem.
- Step one: Turn on extra checks in test environments where the stakes are low
- Step two: Turn them off in production (with realistic data because prod eq. reality) to save cycles
And that seems to be partially accurate. However the truly interesting assertions can test complex conditions that might break complexity (Big O) contracts. Like a private mininum function that is advertised as O(1) on account of taking a sorted list. But there is no type guarantee that the list is sorted. So you assert that it is sorted. But that breaks the complexity contract.
Overall I have not used assertions in Java for trivial conditions in like five years. They're better deployd for something more complex than that.
Then there is the whole thing about -- and more topics to be sure -- crashing the whole application or not. That's not necessarily great for us regular Java programmers. However we can (though discoraged) catch AssertionError if we want to.
https://docs.oracle.com/javase/8/docs/technotes/guides/langu...
And I'm pretty happy with its design considering its age.
Notably this is not a function call and indeed things are not called unless you enable it. Contrast with Zig. So I guess you will only suffer from code bloat if you never enable them.
The tutorial mentions the dangers of side effects. But it also mentions how to use them for more complicated assertions. That's natural since you'll want something like that when you need to check a post-condition.
Programming assertions get joked on because of, ahem.
- Step one: Turn on extra checks in test environments where the stakes are low
- Step two: Turn them off in production (with realistic data because prod eq. reality) to save cycles
And that seems to be partially accurate. However the truly interesting assertions can test complex conditions that might break complexity (Big O) contracts. Like a private mininum function that is advertised as O(1) on account of taking a sorted list. But there is no type guarantee that the list is sorted. So you assert that it is sorted. But that breaks the complexity contract.
Overall I have not used assertions in Java for trivial conditions in like five years. They're better deployd for something more complex than that.
Then there is the whole thing about -- and more topics to be sure -- crashing the whole application or not. That's not necessarily great for us regular Java programmers. However we can (though discoraged) catch AssertionError if we want to.
"And I'm pretty happy with its design considering its age."
Java did the right thing for assertions but then completely failed for the analoguous issue when it comes to logging.
I admit that logging is more complex because you often want it configurable dynamically at runtime. But I'd argue that the language should not be in your way if all you need is a compile time decision and the contortions we made for logging to stay low cost when nothing is logged are crazy in Java.
Java did the right thing for assertions but then completely failed for the analoguous issue when it comes to logging.
I admit that logging is more complex because you often want it configurable dynamically at runtime. But I'd argue that the language should not be in your way if all you need is a compile time decision and the contortions we made for logging to stay low cost when nothing is logged are crazy in Java.
If you want, you can actually use assert for conditional logging (and other conditional program logic).
Few Java programmers are using assertions, the two most important reasons being that it’s difficult to reliably ensure they are enabled in production, and secondly that an Error tends to be too disruptive. Instead, most programmers use always-on defensive checks like requireNonNull() that throw RuntimeExceptions.
Asserts in my Rust code use a custom runtime macro "assert_eq_as_result" which does what the article is describing, by returning Rust Ok or Rust Error.
The Rust crate: https://crates.io/crates/assertables
All the macros have forms for different outcomes:
The Rust crate: https://crates.io/crates/assertables
All the macros have forms for different outcomes:
assert_gt!(1, 2) // panic
assert_gt_as_result!(1, 2) return Result (Ok or Error)
debug_assert_gt!(a, b) // panic when running in debug mode
Asserts in any language must not be added willy-nilly but following a specific methodology viz. Design By Contract (DbC) - https://en.wikipedia.org/wiki/Design_by_contract
DbC was first introduced in Eiffel but the ideas can be used in any language. See the following;
1) Design by Contract and Assertions - https://www.eiffel.org/doc/solutions/Design_by_Contract_and_...
2) Applying "Design by Contract" (pdf) - https://se.inf.ethz.ch/~meyer/publications/computer/contract...
3) Also see the book; Persuasive Programming by Jerud Mead and Anil Shinde which uses asserts systematically to write the proof along with code.
Finally, DbC using asserts is now even more important with AI generated code since it allows one to map the specification to generated code.
DbC was first introduced in Eiffel but the ideas can be used in any language. See the following;
1) Design by Contract and Assertions - https://www.eiffel.org/doc/solutions/Design_by_Contract_and_...
2) Applying "Design by Contract" (pdf) - https://se.inf.ethz.ch/~meyer/publications/computer/contract...
3) Also see the book; Persuasive Programming by Jerud Mead and Anil Shinde which uses asserts systematically to write the proof along with code.
Finally, DbC using asserts is now even more important with AI generated code since it allows one to map the specification to generated code.
As a contrast to Zig: C3 is strongly invested in contracts and is able to use them for static analysis at compile time to some degree.
Right. I remember the C3 thread from a few months ago - https://news.ycombinator.com/item?id=46478647
A user raised some confusion with the wording about Contracts in your documentation which was not answered and is still there. I think it should be fixed since there are lots of people who are confused about contracts and how it differs from error handling. Add to this people's confusion about asserts at runtime and how the optimizer may mess it up and you have a veritable rat's nest of confused thoughts/opinions.
Is your approach to static analysis/verification something like what Frama-C does? I had always wished somebody would wrap C/C++ with a full blown static analysis/verification plus runtime framework and make everything into a single integrated whole like for example the Dafny language. Everything should be doable in a single implementation language with annotations as needed.
A user raised some confusion with the wording about Contracts in your documentation which was not answered and is still there. I think it should be fixed since there are lots of people who are confused about contracts and how it differs from error handling. Add to this people's confusion about asserts at runtime and how the optimizer may mess it up and you have a veritable rat's nest of confused thoughts/opinions.
Is your approach to static analysis/verification something like what Frama-C does? I had always wished somebody would wrap C/C++ with a full blown static analysis/verification plus runtime framework and make everything into a single integrated whole like for example the Dafny language. Everything should be doable in a single implementation language with annotations as needed.
There's more to design-by-contract than asserts, and DbC isn't the only way to use asserts. Most languages lack proper support for design-by-contract.
(For what it's worth I didn't downvote you.)
(For what it's worth I didn't downvote you.)
DbC is the Policy (i.e. what/why) and Asserts are the Mechanism (i.e. how) (https://en.wikipedia.org/wiki/Separation_of_mechanism_and_po...) DbC can be implemented in any language that provides an assert-like mechanism (whether named "assert" or not). An Assert merely validates the state of a program at a particular point during execution. You use it to steer the program to go through only the correct subset of the state space of the program. You could do this pre/post every executable statement (i.e. write proof of correctness) or use a higher-level structured methodology like DbC which is far more practical. The given resources address both.
The point is that when using asserts you think about correctness w.r.t. specifications and nothing else. To think of it as simply validating arguments or in terms of effects on optimization is quite the wrong thing to do.
PS: I don't bother about upvotes/downvotes but am often reminded of the following Sherlock Holmes quote when i see HN's reaction to deeper subjects ;-)
Pshaw, my dear fellow, what do the public, the great unobservant public, who could hardly tell a weaver by his tooth or a compositor by his left thumb, care about the finer shades of analysis and deduction!"
The point is that when using asserts you think about correctness w.r.t. specifications and nothing else. To think of it as simply validating arguments or in terms of effects on optimization is quite the wrong thing to do.
PS: I don't bother about upvotes/downvotes but am often reminded of the following Sherlock Holmes quote when i see HN's reaction to deeper subjects ;-)
Pshaw, my dear fellow, what do the public, the great unobservant public, who could hardly tell a weaver by his tooth or a compositor by his left thumb, care about the finer shades of analysis and deduction!"
> DbC is the Policy (i.e. what/why) and Asserts are the Mechanism
The ideal way to do runtime-checked DbC is not with simple asserts, it's with proper first-class preconditions and postconditions at the language level.
It wouldn't be nice to have to manually ensure that both old and new states of variables are in-scope for postcondition checking. I can imagine that being not just tedious, but error-prone.
> An Assert merely validates the state of a program at a particular point during execution.
Some aspect of the program's state, yes, and hopefully that's all it does.
Interesting to think about the edge-cases here though. Depending on the language, it could accidentally side-effect, or even invoke undefined behaviour, and so actively derail the program. Can't blame DbC for that though, that's a question of language safety.
> You use it to steer the program to go through only the correct subset of the state space of the program
I'm not sure I follow here. You don't use asserts to steer flow-control, you use them to check aspects of program state.
> You could do this pre/post every executable statement (i.e. write proof of correctness)
That doesn't constitute a proof of correctness, no more than last time you and I discussed this. [0] Depending on the language, it wouldn't even necessarily prove the correctness of that particular trace, as you haven't proven that you haven't accidentally invoked undefined behaviour.
You hold a minority opinion on this, please stop presenting it as settled fact.
> The point is that when using asserts you think about correctness w.r.t. specifications and nothing else. To think of it as simply validating arguments or in terms of effects on optimization is quite the wrong thing to do.
I'm not sure why you'd think I don't already know that.
[0] https://news.ycombinator.com/item?id=44675668
The ideal way to do runtime-checked DbC is not with simple asserts, it's with proper first-class preconditions and postconditions at the language level.
It wouldn't be nice to have to manually ensure that both old and new states of variables are in-scope for postcondition checking. I can imagine that being not just tedious, but error-prone.
> An Assert merely validates the state of a program at a particular point during execution.
Some aspect of the program's state, yes, and hopefully that's all it does.
Interesting to think about the edge-cases here though. Depending on the language, it could accidentally side-effect, or even invoke undefined behaviour, and so actively derail the program. Can't blame DbC for that though, that's a question of language safety.
> You use it to steer the program to go through only the correct subset of the state space of the program
I'm not sure I follow here. You don't use asserts to steer flow-control, you use them to check aspects of program state.
> You could do this pre/post every executable statement (i.e. write proof of correctness)
That doesn't constitute a proof of correctness, no more than last time you and I discussed this. [0] Depending on the language, it wouldn't even necessarily prove the correctness of that particular trace, as you haven't proven that you haven't accidentally invoked undefined behaviour.
You hold a minority opinion on this, please stop presenting it as settled fact.
> The point is that when using asserts you think about correctness w.r.t. specifications and nothing else. To think of it as simply validating arguments or in terms of effects on optimization is quite the wrong thing to do.
I'm not sure why you'd think I don't already know that.
[0] https://news.ycombinator.com/item?id=44675668
Yeah, i remember our previous "discussion" on this topic. You were the guy arguing that Formal Method/Verification means only the use of static analysis and verification using SMT/SAT solvers while i was arguing that Formal Methods were far more broader involving multiple levels, a bunch of runtime aspects etc. This is often the easier place to start for programmers since they don't need to learn complex concepts/terminologies initially but can gradually buildup to it. I also note that i gave you a bunch of references in support of my arguments.
> The ideal way to do runtime-checked DbC is not with simple asserts, it's with proper first-class preconditions and postconditions at the language level.
Not quite. DbC should be taught using only simple runtime asserts so that programmers can grasp the essence instead of confusing it with syntactic sugar which is irrelevant to the overall concepts/ideas. Once they grok this they can exercise DbC in any language eg. minimal C language. Furthermore they can now be led to the idea of doing it statically by mapping asserts to verification conditions and thence solved. This can lead to Frama-C and finally to a full-blown verification aware language like Dafny with all the bells-and-whistles.
> It wouldn't be nice to have to manually ensure that both old and new states of variables are in-scope for postcondition checking. I can imagine that being not just tedious, but error-prone.
Dijkstra has already given mechanical transformation rules for this in his wp-calculus. Tedious/error-prone is subjective since for something like a embedded health-monitor it is necessary.
> Some aspect of the program's state, yes, and hopefully that's all it does.
> Interesting to think about the edge-cases here though. Depending on the language, it could accidentally side-effect, or even invoke undefined behaviour, and so actively derail the program. Can't blame DbC for that though, that's a question of language safety.
This is solely the programmer's responsibility and his knowledge of his implementation language. We have already discussed this in our previous discussion.
> I'm not sure I follow here. You don't use asserts to steer flow-control, you use them to check aspects of program state.
An assert is a predicate and therefore an implicit conditional. When true, only a subset of the input state space is allowed in. When false, the program is halted. This is what i mean by "steering" i.e. the running program is a trajectory through a state space which we enforce by the usage of our asserts.
> That doesn't constitute a proof of correctness, no more than last time you and I discussed this. [0] Depending on the language, it wouldn't even necessarily prove the correctness of that particular trace, as you haven't proven that you haven't accidentally invoked undefined behaviour.
> You hold a minority opinion on this, please stop presenting it as settled fact.
We had already discussed this and i had already pointed out that is how "correct-by-construction" approach works whether done informally or formally by a programmer. It is your opinion which is narrow and in certain aspects wrong. Your examples of UB is simply a red herring since i have already pointed out that the programmer needs to be aware of this (and his language's optimizer).
Dijkstra for example invented his GCL and taught his class to use wp-calculus to derive preconditions from postconditions for every executable statement by hand to demonstrate proof of correctness.
> I'm not sure why you'd think I don't already know that.
That was aimed more at the OP article than you. However, when i see your comments w.r.t. UB, i wonder. One needs to know one's language's types and their bounds, sequence points and how it relates to expressions/statements to avoid UB.
> The ideal way to do runtime-checked DbC is not with simple asserts, it's with proper first-class preconditions and postconditions at the language level.
Not quite. DbC should be taught using only simple runtime asserts so that programmers can grasp the essence instead of confusing it with syntactic sugar which is irrelevant to the overall concepts/ideas. Once they grok this they can exercise DbC in any language eg. minimal C language. Furthermore they can now be led to the idea of doing it statically by mapping asserts to verification conditions and thence solved. This can lead to Frama-C and finally to a full-blown verification aware language like Dafny with all the bells-and-whistles.
> It wouldn't be nice to have to manually ensure that both old and new states of variables are in-scope for postcondition checking. I can imagine that being not just tedious, but error-prone.
Dijkstra has already given mechanical transformation rules for this in his wp-calculus. Tedious/error-prone is subjective since for something like a embedded health-monitor it is necessary.
> Some aspect of the program's state, yes, and hopefully that's all it does.
> Interesting to think about the edge-cases here though. Depending on the language, it could accidentally side-effect, or even invoke undefined behaviour, and so actively derail the program. Can't blame DbC for that though, that's a question of language safety.
This is solely the programmer's responsibility and his knowledge of his implementation language. We have already discussed this in our previous discussion.
> I'm not sure I follow here. You don't use asserts to steer flow-control, you use them to check aspects of program state.
An assert is a predicate and therefore an implicit conditional. When true, only a subset of the input state space is allowed in. When false, the program is halted. This is what i mean by "steering" i.e. the running program is a trajectory through a state space which we enforce by the usage of our asserts.
> That doesn't constitute a proof of correctness, no more than last time you and I discussed this. [0] Depending on the language, it wouldn't even necessarily prove the correctness of that particular trace, as you haven't proven that you haven't accidentally invoked undefined behaviour.
> You hold a minority opinion on this, please stop presenting it as settled fact.
We had already discussed this and i had already pointed out that is how "correct-by-construction" approach works whether done informally or formally by a programmer. It is your opinion which is narrow and in certain aspects wrong. Your examples of UB is simply a red herring since i have already pointed out that the programmer needs to be aware of this (and his language's optimizer).
Dijkstra for example invented his GCL and taught his class to use wp-calculus to derive preconditions from postconditions for every executable statement by hand to demonstrate proof of correctness.
> I'm not sure why you'd think I don't already know that.
That was aimed more at the OP article than you. However, when i see your comments w.r.t. UB, i wonder. One needs to know one's language's types and their bounds, sequence points and how it relates to expressions/statements to avoid UB.
[deleted]
Very interesting write-up, thank you! I never really considered that compilers can also use asserts to improve performance, but it does make sense.
> Imagine a big codebase with this somewhere in it:
fn processThing(thing: Thing) void {
// this function must always be invoked on
// a thing that has already been started
assert(thing.is_started);
// ...
}
The "assert" word is not a great choice, but it's entrenched that way. In a debate, you'd not want to assert something (present it as a fact) if you're not sure.
Optimization promises have the same form; they are also assertions, but with a different purpose. They can use the same syntax, but some different word.
The word assert is attractive for this purpose: I know for sure something is true, and I'm communicating it to the compiler; thus, I am asserting something.
The designer must not be thereby seduced into conflating debugging assertions with optimization promises.
I understand that in this case they have a safety switch for assertions, but conflating debug assertions with optimization promises by means of a switch is still a poor design.
You want that switch on a case-by-case basis for each individual assertion, and the easiest way for that is to just have a different identifier.