YHK - yet another hacker news clone

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.

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.

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.

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.

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.

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 :)

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:

https://gavinray97.github.io/blog/design-by-contract-and-eff...

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 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.

Since this is for C++26, you use modules.

Strictly speaking you put them in the header.

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.

they are literally meant to be better asserts, that can be shown on a function declaration.

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.

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.

    pre(x >= 0)

    pre(y >= 0)

    return x + y;

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.

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. Don’t expect them to be like LiquidHaskell.

No worries, this will probably land in C as well, static_assert was already.

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.

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.