4 ms·

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

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

accelbred 2y ago
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.
- kelnos 2y ago
  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.
- pdimitar 2y ago
  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.
  - kstrauser 2y ago
    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.
- SkiFire13 2y ago
  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.
- sunshowers 2y ago
  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.
blub 2y ago
> 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.
- sunshowers 2y ago
  Completely reasonable.
- dralley 2y ago
  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.
  - blub 2y ago
    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.
  - rileymat2 2y ago
    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.
    - 2y ago

accelbred 2y ago

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.

kelnos 2y ago
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.
pdimitar 2y ago
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.
- kstrauser 2y ago
  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.
SkiFire13 2y ago
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.
sunshowers 2y ago
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.

blub 2y ago

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

sunshowers 2y ago
Completely reasonable.
dralley 2y ago
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.
- blub 2y ago
  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.
- rileymat2 2y ago
  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.
  - 2y ago