Hacker News

points by nanolith 4 days ago | 0 comments

While I can understand that C++ contracts were met with controversy, contract annotations scoped at analysis time that can be verified by external tools, such as static analyzers, model checkers, or automatic theorem provers, are incredibly useful.

I put together an alternative function contract and invariant mechanism in C using CBMC and custom macros that effectively allows me to perform formal methods in C using compositional verification. The reason why I chose C is because of its relative simplicity and relative ease of building tooling around it. C++ contracts provide some feature parity, and would let me take advantage of some of the features in C++ relative to C.

I hope that the contract proposal is workshopped and simplified so it can be proposed again for a future version. Its current form is unsuitable, but it deserves a second chance with a simpler implementation. Contracts would narrow the safety gap between C++ and languages such as Ada / SPARK.

[–] uecker 4 days ago

C and formal verification is an awesome combination. I tried cmbc on some toy programs, it it fully automatically proved memory safety and all assertions. But for larger programs one has to split up with a contract-like facility.

Can you tell us more how you use cbmc with macros? I am also exploring this.

I also wonder what feature from C++ you miss in C?

[–] Surac 4 days ago

Well i you ask me i miss namespaces and functions i could put into struct and enum types

[–] nanolith 3 days ago

I did a talk on this at BSDCan 2026:

https://www.bsdcan.org/2026/timetable/timetable-Model-Checki...

That link has the slides and some example code. There's also a live stream on YouTube.

Regarding features I miss from C++, I like the concept of generics. I don't like the implementation in C++. I also find C's _Generic facility to be limited, especially when building containers that perform hygienic type erasure. This feature isn't enough for me to go back to C++ on its own, but it is something I'm exploring in a new language I'm writing.

[–] uecker 2 days ago

Thank you!

[–] locknitpicker 4 days ago

> contract annotations scoped at analysis time that can be verified by external tools, such as static analyzers, model checkers, or automatic theorem provers, are incredibly useful.

Yes they would be.

Except that's not the contracts that they tried to force down C++'s throats.

The current contracts proposals features things like throwing exceptions in contract predicates, leaves out basic features such as function pointers, and not to mention that the contract specification alone covers around 5-10% of C++ specification and still glances over most details as being implementation defined.

As everyone is attacking Stroustrup as this master mind behind this opposition, perhaps people should devote some time to read one of the many papers pointing out the many flaws in the proposal. Stroustrup himself features as the coauthor of a few of them. Why is this not a technical discussion but a witch hunt?

[–] materielle 4 days ago

As somewhat of an outsider, the C++ spec process seems really strange to me.

It’s weird that major features are designed from start to finish without even having so much as a demo.

It feels like there should be a back and forth process between committee proposal -> experimental impl in a major compiler -> community feedback, and so on.

It sounds like it’s basically the waterfall approach to language design? They write a glorious spec and chuck it out to the world, and hope that compilers can implement it and people actually find it useful. Example: modules.

[–] locknitpicker 4 days ago

> It’s weird that major features are designed from start to finish without even having so much as a demo.

Not necessarily. In broad terms, Boost is considered a staging ground for features proposed to C++. Compiler projects also keep up with the standards.

In this case the concept guys continuously dropped the ball on this requirement though. One of the papers pointing the many flaws in the proposal calls out this shortcoming, where contracts have neither a workable reference implementation nor an adequate specification. In fact, they handwaved a lot over details with vague calls to "implementation-defined".

[–] MFHava 3 days ago

> contract specification alone covers around 5-10% of C++

I have no idea where you read that but it is a blatant lie - easily disproven by the way: N5046 which is pretty close to the C++26 DIS has 2668 pages. P2900R14 has a total of 114 pages, of which ~56 pages are dedicated to proposed wording.

Wording is presented as a diff to the working draft and contains extensive copies of the existing text that is either amended, modified or removed. (Aka: there are no 56 pages of wording).

[–] twhitmore 4 days ago

Contracts are useful, but don't guaranteed anything if type safety & memory safety can be bypassed.

I think the ISO panel made the right call. The real world consider memory safety & execution integrity to already be critical issues (and C++ no longer to be viable), and they are correct. The WG has its priorities wrong.

[–] uecker 4 days ago

Memory safety can also be bypassed in Rust. If you want something where memory safety is guaranteed, use Fil-C but this comes at a performance cost. Or use formal verification, where then contracts can help (but C++'s complexity doesn't).

[–] saghm 4 days ago

This is like responding to someone saying that someone can die from an getting shot accidentally by a gun by saying you can also die from drinking too much water. Both of them are technically true and do happen on occasion, but one of them is not nearly as much of a risk in most circumstances, whereas the other is pretty much inherent to the most basic way of using it.

[–] uecker 4 days ago

No, I do not think that this is comparable. This just the annoying exaggeration I complain about. In reality, one can write fairly safe C code, while Rust code in practice is also far from perfectly safe and also introduces new supply chain risks.

[–] saghm 4 days ago

I don't agree at all.

> one can write fairly safe C code

In practice, pretty much every C/C++ codebase in existence has ended up having memory safety issues, even very widely used ones with a lot of scrutiny over the years.

> while Rust code in practice is also far from perfectly safe and also introduces new supply chain risks.

You're conflating "does not have one notoriously dangerous type of safety issue" and "does not have any safety issues", which is a disingenuous characterization of what I said. You were the one who introduced the comparison to memory safety in Rust and C++, and now you're moving the goalposts as an attempt to rebut my disagreement.

[–] uecker 3 days ago

I know you disagree. But I am not conflating anything. You just claim that C is unsafe and any issue we see is obviously evidence for this, while Rust is safe and any issue we see does not change this. But there is no logical argument here that makes sense. In reality, projects in both languages see issues in practice, and to decide whether the safety is much better in one or the other can only be decided by a careful analysis based on some risk model. Note that I do no deny that Rust has an advantage with regard to memory safety (and instead a huge supply chain problem), I am just saying the advantage is massively exaggerated (and the arguments are largely based on unfair comparisons and bad statistics).

[–] uecker 3 days ago

A comparison which would be more accurate in my opinion is to look at driving in the 1960: Not much have built-in safety and no compulsory seat-belts (we see many issues with C/C++ projects, often very easy to fix). One can also even claim that no driver can safely control a car in all circumstances ("not even experts can use C safely"). Yet, with modern cars and regulations, driving is much safer today than it was and can be considered reasonably safe (modern C code and modern tooling). Rust proponents claim we must give up driving with cars completely because it too dangerous (all the accidents are clear evidence) and we must switch to trams as it is impossible to steer them into some objects (and even though there are also still accidents, trams have "steering safety" and rule out a whole class of driver errors).

You don't have to agree, but this is how I see it.

[–] saghm 3 days ago

> But I am not conflating anything. You just claim that C is unsafe and any issue we see is obviously evidence for this

That is explicitly not what I'm claiming. You seem to think that I think "memory safety" is equivalent to "safety", which is what I've repeatedly told you is not what I'm saying. That's conflation. It's not clear why you'd expect me to read more details you give after repeatedly ignoring what I'm saying and putting words in my mouth that I'm not saying, so I have to assume at this point you're posturing for other readers rather than actually trying to communicate with me in any reasonable way.

[–] tkz1312 4 days ago

I was surprised to discover recently that C++ is in a pretty nice sweet spot for verification (at least at the binary level), where it has some useful type system features, but will get out of your way and generate simple ASM (without e.g. spamming bounds checks and panics everywhere as rust does).

[–] nanolith 3 days ago

Any language is viable if appropriate engineering is applied to it. There are many billions of lines of code in C and C++. This software needs to be made safer, and it is not possible nor viable to rewrite it all into a different language. Hence, we need to dig into CS and PL theory to find ways to fix this software that does not incur significant investment, does not require retraining software developers in a new language, and does not result in a "big rewrite in the sky" style project.

Contracts are annotations, much like types are. What makes contracts powerful is the tool that examines this annotation, as is the case with types. A type checker, such as an H-M type checker, can only perform limited checks. It's possible to use a dependent type checker with dependent types, but this is undecidable, and it requires a proof assistant and human guided tactics to resolve. In practice, this is expensive, and when automation such as LLMs are used, one currently gets tactic soup that is difficult to understand, which defeats the purpose.

A model checker, such as CBMC or ESBMC, can work with contracts to verify specification that would be difficult to verify without contracts. Model checkers can already verify memory safety and even the absence of memory leaks across an entire program. However, model checking grows exponentially expensive as we add more code to be verified. Contracts give us the ability to perform compositional verification, which allows us to verify codebases into the millions of lines of code or larger by breaking down this verification into many small model checks, stitching these together with contracts and invariants. Contracts and invariants complement type checking and significantly extend it. It's possible to use contracts and invariants to add these checks to an untyped language or a minimally typed language such as C. If my precondition includes the data invariant, "property_valid_widget(x)", then effectively, this also type checks x. This works even if I've completely erased the type and later recast it.

The "real world" doesn't currently have a solution for reducing general software safety issues -- which goes far beyond memory safety -- other than formal methods. Practical and efficient ways to formally verify software is within our reach, and is already being done with other languages. I do this today with C / CBMC using contracts and invariants. I get memory safety, specification safety, and a guarantee of no memory leaks. This can also be done with C++, Rust, Java, and other languages using similar techniques. While it is true that Rust and Java both have basic memory safety in place, they also both can harbor vulnerabilities that could be resolved with function contracts and model checking.

Contracts are more than useful; they give visibility of developer intent to model checkers and similar tools. This visibility makes software significantly safer than borrow checking or type checking can alone.