Hacker News Reader

Comment by sunshowers | Hacker News Reader

> Proper tooling with C can prevent memory issues, taking away the main argument for rust.

This is not true, despite decades of research and billions of dollars poured into static analysis of C programs. Rust solves this by making programmers put pervasive annotations into their code, and even more importantly by making programmers like the fact that they have to put pervasive annotations into their code. Rust today, without additional tooling, delivers a better memory safety story than C static analysis researchers could ever dream about.

View on HN

> even more importantly by making programmers like the fact that they have to put pervasive annotations into their code

That’s the thing: many of us deeply dislike the annotations since they slow things down and look ugly.

Completely reasonable.

Many developers dislike doing all sorts of useful things, like writing documentation in general, or tests.

Rust is an upfront investment of time which pays back in later stages when you're not spending 10 hours hunting down issues with valgrind or trying to explain codebase-specific lifetime semantics to junior developers. Yes the initial development is "slower", but you can then do massive refactors without fear of breaking some subtle rule that will blow things up, because such rule-breaking would result in a failure to compile.

I must write code very differently than most writing the actual code is not what takes my time. Sure you feel that time, but it ends up being a pretty small percentage of mine.

So? I feel like that backs up my point. Sure it may slow down development but it encodes useful information for reading and understanding the code later on, and preventing the most pernicious sorts of bugs (data races, UB, memory unsafety) from creeping in in the first place - and thus less need to spend time doing non-development tasks later.

Yes, I am agreeing. I am saying, a lot of these affordances that enter code faster or terser are not where I spend my time. I spend my time on the things you are talking about.

Rust is a continuous additional investment of time which will need to happen when writing the code, changing the code, doing the massive refactorings you mention and last but not least when reading the code.

There are benefits to that investment, but likely only in specific kinds of software (such as browsers, kernels, etc) which are relentlessly attacked and for specific kinds of programmers that like to specify things in much detail and don’t mind the associated costs.

The friction comes from pushing Rust as a generic solution for most programmers. See the Rust in the backend efforts for the perfect example.

This is false; with formal analysis tools like CBMC, you can prove the memory safety properties of your C code. You can even statically prove lack of integer overflows and that asserts are unreachable. I'll agree this is uncommon in general, but CBMC is used for various C codebases where I work. Though this tooling is also available for Rust with Kani.

Is CBMC usable, directly, on any project? Or do you need to write your code in a certain way, using certain patterns, etc.? Or does the CBMC tooling need to be taught various things about how memory management works in your project?

Regardless, the fact that it's not used regularly/routinely with the Linux kernel (or any project that I'm aware of) suggests that it's either not suitable, doesn't catch enough issues to be worth the effort, or is just such a pain to deal with that no one has the patience to put up with it.

Rust gives you much (sure, not all) of what CBMC provides, in the compiler. That is a huge win, IMO.

Yet it's still not used in most C codebases. Where was it for Heartbleed?

We all understand that things can be done better. The problem is that they often are not.

Rust and other tools help by not giving people the choice to do sloppy work at all. History has proven many times that defaults matter.

That’s the crux of it. I think I can write safe C. So do many other people who, surely like me, cannot. I know I’ve written safe Rust because I had to fix my code until it was able to compile.

I think the issue with such formal analysis tools is that in order to make the analysis succeed you often end up writing code that doesn't look like normal C anymore and arguably at that point you're not writing C anymore.

---

As an aside, does CBMC check temporal memory safety and thread safety? It seems it checks for out-of-bound accesses, null pointer access and double-free, but I could not find a mention of use-after-free and data races.

CBMC is truly wonderful technology. Rust is still more powerful and easier to use at scale.

If your project has 100k lines of code, would you rather use CBMC or Rust? What about if your project has a million? 10 million? 100 million?

The fundamental issue is that SMT-based verification scales quite poorly. The optimal use of SMT-based verification is proving local properties of small chunks of code independently, and using the type system's encapsulation to scale up to global correctness.

Reply on news.ycombinator.com