Comment by tialaramex
4 days ago
Contracts are a way to express invariants, "This shall always be true".
There are three main things you could do with these invariants, the exact details of how to do them, and whether people should be allowed to specify which of these things to do, and if so whether they can pick only for a whole program, per-file, per-function, or whatever, is separate.
1. Ignore the invariants. You wrote them down, a human can read them, but the machine doesn't care. You might just as well use comments or annotate the documentation, and indeed some people do.
2. Check the invariants. If the invariant wasn't true then something went wrong and we might tell somebody about that.
3. Assume these invariants are always true. Therefore the optimiser may use them to emit machine code which is smaller or faster but only works if these invariants were correct.
So for example maybe a language lets you say only that the whole program is checked, or, that the whole program can be assumed true, or, maybe the language lets you pick, function A's contract about pointer validity we're going to check at runtime, but function B's contract that you must pick an odd number, we will use assumption, we did tell you about that odd number requirement, have the optimiser emit that slightly faster machine code which doesn't work for N=0 -- because zero isn't an odd number assumption means it's now fine to use that code.
I guess the reason I found it surprising is that I would only use 3 (ie risk introducing UB) for invariants that I was very certain were true, whereas I would mostly use 2 for invariants that I had reason to believe might not always be true. It struck me as odd that you'd use the same tool for scenario's that feel like opposites, especially when you can just switch between these modes with a compiler flag
It feels pretty clear to me that these Contracts should only be used for the “very certain” case. Writing code for a specific compiler flag seems very sketchy, so the programmer should assume the harshest interpretation.
The runtime check thing just sounds like a debugging feature.
In other words, in production mode it makes your code faster and less safe; in debug mode it makes your code slower and more safe.
That's a valid trade-off to make. But it's unexpected for a language that bills itself as "The Ergonomic, Safe and Familiar Evolution of C".
Those pre/post-conditions are written by humans (or an LLM). Occasionally they're going to be wrong, and occasionally they're not going to be caught in testing.
It's also unexpected for a feature that naive programmers would expect to make a program more safe.
To be clear this sounds like a good feature, it's more about expectations management. A good example of that done well is Rust's unsafe keyword.
> That's a valid trade-off to make. But it's unexpected for a language that bills itself as "The Ergonomic, Safe and Familiar Evolution of C".
No, I think this is a very ergonomic feature. It fits nicely because it allows better compilers to use the constraints to optimize more confidently than equivalently-smart C compilers.
I'll give you "more ergonomic" if you'll give me "less safe".
2 replies →
Maybe also worth mentioning is that some static analysis is done using these contracts as well. With more coming.
Is C3 using a different terminology than standard design by contract?
Design by contract (as implemented by Eiffel, Ada, etc.) divides the set of conditions into three: Preconditions, postconditions, and invariants. Pre- and postconditions are not invariants by predicate checks on input and output parameters.
Invariants are conditions expressed on types, and which must be checked on construction and modification. E.g. for a "time range" struct with start/end dates, the invariant should be that the start must precede the end.
So the compiler could have debug mode where it checks the invariants and release mode where it assumes they are true and optimizes around that without checking?
Yes, and that same pattern already does exist in C and C++. Asserts that are checked in debug builds but presumed true for optimization in release builds.
Not unless you write your own assert macro using C23 unreachable(), GNU C __builtin_unreachable(), MSVC __assume(0), or the like. The standard one is defined[1] to either explicitly check or completely ignore its argument.
[1] https://port70.net/~nsz/c/c11/n1570.html#7.2
1 reply →
You've described three different features with three different sets of semantics. Which set of semantics is honored? Unknown!
This is not software engineering. This is an appeal to faith. Software engineering requires precise semantics, not whatever the compiler feels like doing. You can't even declare that this feature has no semantics, because it actually introduces a vector for UB. This is the sort of "feature" that should not be in any language selling itself as an improved C. It would be far better to reduce the scope to the point where the feature can have precise semantics.
> Which set of semantics is honored?
Typically it's configurable. For example C++ 26 seems to be intending you'll pick a compiler flag to say if you want its do-nothing semantics, or its "tell me about the problem and press on" semantics or just exit immediately and report that. They're not intending (in the standard at least) to have the assume semantic because that is, as you'd expect, controversial. Likewise more fine-grained configuration they're hoping will be taken up as a vendor extension.
My understanding is that C3 will likely offer the coarse configuration as part of their ordinary fast versus safe settings. Do I think that's a good idea? No, but that's definitely not "Unknown".
Any idea how the situation is handled where third party code was written to expect a certain semantic? Is this just one more rough edge to watch out for when integrating something?
not enforced for any given implementation is hardly "unknown". presumably the tin comes with a label saying what's inside