I'm all for signing up for a contract if it can turn a runtime error into a compile time error. However, this looks like it just makes more runtime errors. At that point, these seem no better than `assert` except for the fact that they promise to really assert (probably).
The article also points out a big problem which is "Importantly, this aspect of Contracts is why contract assertions must not be used for error handling and input validation: If a function has in-contract requirements to report certain events as errors, that handling must be done with standard C++ control statements that are not optional, never with contract assertions."
That sort of muddy definition of what contracts are supposed to be used for is almost certainly going to make a mess. It's not input validation, but parameter validation.. but not really validation but rather checks which error out, but it's not errors we are producing.
It’s a standard way to do pre and post conditions. Clojure pre and post conditions also behave this way. If you force these conditions into compile-time checks, well, then you are introducing a second type system with refinement types into the language. And type checking would take a long time. Imagine someone writes a precondition for a function where its integer argument x needs to satisfy collatz(x)==1; do you now expect the compiler to prove the collatz conjecture or verify it for all 64-bit integers every compilation?
My experience using pre and post conditions in Clojure makes me really like them. They are a small but meaningful improvement over plain old assertions. And yes being able to turn them off is a feature not a bug.
contracts are intended to document hoare logic. i.e. pre, post, invariant.
They can be compile time if the compiler can verify them statically (where they become a noop), runtime otherwise, or disabled entirely if you can't prove them statically but don't want the overhead cost.
Realistically contracts will gradually evolve towards static/compile time asserts as tooling improves.
And like the blog post states, contracts are explicitly not input validation. They are there to encode what you expect and what you don't internally in your code rather than just documenting those pre/post/invariant conditions in comments.
> Contracts are explicitly not input validation. They are there to encode what you expect
The line between what's "input validation" and what's "What you expect" is very muddy. Input validation is a statement of "this is input I expect".
Is it input validation to say a string must be at least some length characters? What if that string is a password? What if it's an MD5 sum?
It SHOULDN'T be used for input validation but it will be. And almost certainly the person that does use it for input validation will argue that they were just laying out expectations.
The bit about contracts not being input valuation is no different than the case for assertions. It's basically saying that if assertions were inappropriate, so are contracts. So if you find that like blurry, the blurriness predates contracts.
That said, the distinction is generally pretty clear: an assertion failure (and therefore a contract failure) indicates a bug. It must never happen, and therefore it must always be OK to suppress the validation. If you see it fire, that's a bug report, and your code needs fixing. And if your contract to the caller is that you will enforce some constraint on them (as opposed to assuming they already took care of ensuring it), then you need the validation in your runtime code.
They are basically asserts that you can put in headers. Which is great because asserts are usually useless to IDEs because you only get the headers for libraries.
And with the 'observe' mode you can turn them on in production code right away and collect data without a failed assert terminating.
Well, except for the fact that asserts can be used during debugging to do input validation while these shouldn't be used for that. They also introduced `contract_assert` which seems to have no benefit over assert other than it's more likely to not be disabled.
Rust is quite complicated but people like it a lot. Python too in a way - it's quite large and complicated but it exposes the complexity in a very gradual way and you can ignore so much of the language and still get things done.
I agree with you about simple languages though. I really like Go - the "there should be only one way to do things" from the Zen of Python actually applies to Go in a way that it doesn't apply to Python at all.
Languages like Go, is how you end up with what appears simple on the surface, while in reality is full of gotchas and boilerplate for what complex languages support out of the box.
That is how you get double nils, exception handling that pretends not to be one, url based imports that requires source code and rewrites when the host changes, generators by code patterns, generics that miss some language constructs,....
On the one hand, almost everyone (including C++ fans) agrees that the language is too big. On the other hand, comtracts just formalize an existing and useful concept.
If you enjoy this style of programming, I wrote a bit on why contracts and capabilities (ie "allocates memory", "performs i/o") are going to become essential for LLM generated code:
I am very bullish on constraints based programming like this.
The main problem is code organization and syntax. Tacking stuff like this onto fuction declarations is too basic.
Ideally, I think we need better constructs, e.g. dettached constraints like to the function declaration. You can define constraints separately, in the same namespace or w/e, add notes, comments, etc. and the function declaration can be used with intellisense to jump to the constraint. You could even tag the defintions.
In modern AI-based workflows, the agent can pull up an explanation on the function, and point directly to the constraints, with strong confidence esp. if it's got explicit metadata.
Take a look at Racket (or Rhombus if allergic to parens). Support for contracts there is stellar and provides everything you mentioned. You can use `define/contract` for inline contracts, or you can attach contracts when exporting names from a module using `contract-out` declaration. Contracts are first-class, can be defined separately and attached wherever you want (importantly, this includes values (structs, classes) as well as functions). There are higher-order contracts that generate new contracts from existing ones. There's support for both static and dynamic metadata for almost all kinds of entities in code (ie. both the syntax and the semantic entity it produces can be annotated with anything). I wouldn't recommend using Racket/Rhombus in production, but it's a great preview of what might become commonplace in a decade or two :)
The article makes no mention of optimisation use cases. In case anyone already knows off the top of their heads and before I start digging for the answer, is part of the intent here for these to inform the optimiser stages, perhaps similarly to what the if (!(some_condition)) { __builtin_unreachable(); } idiom can achieve?
Allegedly the pre and post conditions, in varying degrees of certainty according to the evaluation semantics selected, are propagated to the optimization passes of gcc and llvm. However, I haven’t seen any detailed blog posts or summaries of the effectiveness or reliability of this feature. Sorry it’s not a lot of info, but it was what I knew off hand based on previous reading.
If I put them in the header, I have to include half the world because I can't forward declare `Foo foo` argument if I want to check `foo.size() > 3` or similar in a pre/post-condition. This is a non-starter, keeping headers lean is the only way to not end up with 1 hour compiles.
If I put them in the cpp, they lose their only advantage over asserts - that they also double as documentation in the headers.
Did we add 50 pages to the standard for a slightly fancier assert? I feel like this could've been one builtin and a footnote:
contract_assert(expr) - if expr evaluates to false, the behavior of the program is undefined. Implementations are encouraged to emit a runtime check for this in debug builds, or a compiler error in cases where they can statically determine, that the assert will fail.
The first declaration of a function must include the contract pre/post conditions and follow-up re-declarations of the function must either not include any contract conditions or the same conditions as the initial declaration.
And you can avoid re-including the world because pre/post conditions should be externally visible behavior or call out to functions for pre/post checks on internal behavior.
Essentially you either define them using what you have in scope during the initial declaration or you call out to a function located elsewhere that can have access to more/internal scope and do more complicated checks.
I'm expecting to see talks (and buy books, read blogs...) in 3 years by someone who spent a lot of work adding contracts to a small but significant code base. This is the type of question they will answer.
I think the right answer is in the header, and in turn that means someone needs to answer your objection - how do you avoid long compiler times? I suspect modules is a large part of the answer, which means the guide/talk will also be how to make modules work in the real world. Remember though, that is all guesses I wouldn't be surprised if I'm wrong.
I'm looking forward to seeing where these go in the future. Can solvers prove my code correct (at least in some trivial cases)? What should happen in a unit test (sometimes I want to test that my program handles out of range values, sometimes it is expensive top check and so I put the contract in to avoid the check at runtime...) Can/should the optimizer account for contracts (same question as unit tests).
See the papers "Soft Contract Verification" and "Soft Contract Verification for Higher-Order Stateful Programs" (Nguyễn et al.) In general, there's a lot of academic work on the topic coming from the Racket community.
In short: yes, some classes of contracts can be statically proven. Not all of them, and it depends on the language's semantics, so it's probably not easy to retrofit into C++. But there's work being done on unifying types and contracts, moving back and forth between static proof and dynamic enforcement, and it's all pretty interesting. Proving contracts statically eliminates runtime overhead; generating contracts from types makes it possible for a gradually typed language to be sound.
I haven't seen those papers. The general thought seems to be that progress is good enough that a restricted subset of C++ can be proved (which is getting less restricted all the time, though probably never will be everything) and the solvers will be able to detect where they give up: if you want a solver you will have to write the code they can prove and that is an acceptable limitation.
Contracts also allow a solver to say "I can't prove this messy function, but I can at least prove everything around it". Which is to say if we prove the precondition is met, and if we assume the post conditions are met, we can prove everything else despite the messy parts we can't do. This at least lets us know where the messy code is.
I can see the appeal of having 'code as documentation' in header files, but personally I find any type of runtime asserts to be too heavy handed. Graceful error handling, in my opinion, is always preferable. This type of functionality is what is continuing to drive me away from C++. If your preconditions and postconditions matter, document them in a comment block.
Graceful handling is a trade off. Sometimes the check is expensive, if everybody normally does it right you don't want to check (particularly in a tight loop), but you don't want to lose this. I work in embedded, in production our CPUs are not powerful enough to risk all those runtime checks, but I want to turn them on when I work on my workstation - in hopes that if there is a problem we catch it.
Contacts are also a guaranteed syntax. Runtime checks provide no way for tools to know if the condition is expected to never happen - this is a bug; vs this is a normal user error we need to check for. A contract means theorem provers can find code paths where a bug could happen - of course we don't have theorem provers for C++, but this is seen as a requirement to get them.
You can set a "contract evaluation semantic" for contracts. One of them is "observe", which only prints a message on contract violations. With "ignore", nothing at all happens.
From the "C++ design committee was so preoccupied with whether they could, they never stopped to think whether they should" department.
Asserts:
1. You don't like the being conditional on NDEBUG ot aborting the program - roll out your own. Will still be a one-liner.
2. You want them act as documentation of pre-conditions in headers - just add a bloody comment there.
The only somewhat reasonable development here are the post conditions in functions with multiple returns, but post/s are dramatically less common than pre/s, so their utility is also debatable.
I have seen far too many times when the comment in the implementaiton doesn't match reality to accept pre/post conditions in a comment. I want my contracts someplace where they get evaluated from time to time so that they are fixed when they are wrong.
An anthropic employee did a talk earlier this year or last and i think it was said that yeah, they eat it up. Tools to find errors because it is visible is great
I'm all for signing up for a contract if it can turn a runtime error into a compile time error. However, this looks like it just makes more runtime errors. At that point, these seem no better than `assert` except for the fact that they promise to really assert (probably).
The article also points out a big problem which is "Importantly, this aspect of Contracts is why contract assertions must not be used for error handling and input validation: If a function has in-contract requirements to report certain events as errors, that handling must be done with standard C++ control statements that are not optional, never with contract assertions."
That sort of muddy definition of what contracts are supposed to be used for is almost certainly going to make a mess. It's not input validation, but parameter validation.. but not really validation but rather checks which error out, but it's not errors we are producing.
My experience using pre and post conditions in Clojure makes me really like them. They are a small but meaningful improvement over plain old assertions. And yes being able to turn them off is a feature not a bug.
They can be compile time if the compiler can verify them statically (where they become a noop), runtime otherwise, or disabled entirely if you can't prove them statically but don't want the overhead cost.
Realistically contracts will gradually evolve towards static/compile time asserts as tooling improves.
And like the blog post states, contracts are explicitly not input validation. They are there to encode what you expect and what you don't internally in your code rather than just documenting those pre/post/invariant conditions in comments.
The line between what's "input validation" and what's "What you expect" is very muddy. Input validation is a statement of "this is input I expect".
Is it input validation to say a string must be at least some length characters? What if that string is a password? What if it's an MD5 sum?
It SHOULDN'T be used for input validation but it will be. And almost certainly the person that does use it for input validation will argue that they were just laying out expectations.
This only happens during constant evaluation. For example, the following could be determined statically, but compiles w/o error on gcc
int add_nums(int x, int y)
{ }int result_rt = add_nums(-1,-1); // no compile error
That said, the distinction is generally pretty clear: an assertion failure (and therefore a contract failure) indicates a bug. It must never happen, and therefore it must always be OK to suppress the validation. If you see it fire, that's a bug report, and your code needs fixing. And if your contract to the caller is that you will enforce some constraint on them (as opposed to assuming they already took care of ensuring it), then you need the validation in your runtime code.
And with the 'observe' mode you can turn them on in production code right away and collect data without a failed assert terminating.
It includes checkpoint semantics (something that is part of contracts in general) as well as processing through the contract violation handlers.
Functionally contract_assert should eliminate the need to use assert at all and is an over all substantial UX improvement.
https://gavinray97.github.io/blog/adding-invariant-to-cpp-de...
The post turned out to be more useful for an intro to writing GCC plugins than anything, but at least I had fun
If I’m going to write code by hand, the requirement for a beautiful pleasant language is bigger than ever.
I agree with you about simple languages though. I really like Go - the "there should be only one way to do things" from the Zen of Python actually applies to Go in a way that it doesn't apply to Python at all.
That is how you get double nils, exception handling that pretends not to be one, url based imports that requires source code and rewrites when the host changes, generators by code patterns, generics that miss some language constructs,....
https://en.wikipedia.org/wiki/Design_by_contract
https://www.eiffel.com/values/design-by-contract/introductio...
https://gavinray97.github.io/blog/design-by-contract-and-eff...
The main problem is code organization and syntax. Tacking stuff like this onto fuction declarations is too basic.
Ideally, I think we need better constructs, e.g. dettached constraints like to the function declaration. You can define constraints separately, in the same namespace or w/e, add notes, comments, etc. and the function declaration can be used with intellisense to jump to the constraint. You could even tag the defintions.
In modern AI-based workflows, the agent can pull up an explanation on the function, and point directly to the constraints, with strong confidence esp. if it's got explicit metadata.
If I put them in the header, I have to include half the world because I can't forward declare `Foo foo` argument if I want to check `foo.size() > 3` or similar in a pre/post-condition. This is a non-starter, keeping headers lean is the only way to not end up with 1 hour compiles.
If I put them in the cpp, they lose their only advantage over asserts - that they also double as documentation in the headers.
Did we add 50 pages to the standard for a slightly fancier assert? I feel like this could've been one builtin and a footnote:
contract_assert(expr) - if expr evaluates to false, the behavior of the program is undefined. Implementations are encouraged to emit a runtime check for this in debug builds, or a compiler error in cases where they can statically determine, that the assert will fail.
The first declaration of a function must include the contract pre/post conditions and follow-up re-declarations of the function must either not include any contract conditions or the same conditions as the initial declaration.
And you can avoid re-including the world because pre/post conditions should be externally visible behavior or call out to functions for pre/post checks on internal behavior.
Essentially you either define them using what you have in scope during the initial declaration or you call out to a function located elsewhere that can have access to more/internal scope and do more complicated checks.
I think the right answer is in the header, and in turn that means someone needs to answer your objection - how do you avoid long compiler times? I suspect modules is a large part of the answer, which means the guide/talk will also be how to make modules work in the real world. Remember though, that is all guesses I wouldn't be surprised if I'm wrong.
In short: yes, some classes of contracts can be statically proven. Not all of them, and it depends on the language's semantics, so it's probably not easy to retrofit into C++. But there's work being done on unifying types and contracts, moving back and forth between static proof and dynamic enforcement, and it's all pretty interesting. Proving contracts statically eliminates runtime overhead; generating contracts from types makes it possible for a gradually typed language to be sound.
Contracts also allow a solver to say "I can't prove this messy function, but I can at least prove everything around it". Which is to say if we prove the precondition is met, and if we assume the post conditions are met, we can prove everything else despite the messy parts we can't do. This at least lets us know where the messy code is.
Contacts are also a guaranteed syntax. Runtime checks provide no way for tools to know if the condition is expected to never happen - this is a bug; vs this is a normal user error we need to check for. A contract means theorem provers can find code paths where a bug could happen - of course we don't have theorem provers for C++, but this is seen as a requirement to get them.
From the "C++ design committee was so preoccupied with whether they could, they never stopped to think whether they should" department.
Asserts:
1. You don't like the being conditional on NDEBUG ot aborting the program - roll out your own. Will still be a one-liner.
2. You want them act as documentation of pre-conditions in headers - just add a bloody comment there.
The only somewhat reasonable development here are the post conditions in functions with multiple returns, but post/s are dramatically less common than pre/s, so their utility is also debatable.