Hacker News
points by twhitmore 4 days ago | 0 comments
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.

[–] uecker 3 days ago
I do not think there are other readers in this thread anymore for which I could posture. You are right that I should not introduced other safety issues into the discussion. Still I am not following. Clearly contracts allow one to guarantee memory safety of a function. The original argument was that this does not count because there are ways around it, to which I responded that Rust also has ways around it. Your point seemed to be that the risks are vastly different and I think this is an exaggeration.

But maybe I am still not getting your point correctly.

[–] 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.