5 ms·

A static checker for C code can do the similar checks that the borrow checker in Rust does. Essentially it enforces a variation of linear type system. Note that

A static checker for C code can do the similar checks that the borrow checker in Rust does. Essentially it enforces a variation of linear type system. Note that many things for Rust are on ideas from Cyclone [1], that was a research project to provide minimal extensions to C type system to ensure memory safety. [1] - https://cyclone.thelanguage.org/ https://cyclone.thelanguage.org/

pjmlp 9y ago
Only works if 100% of the code is available, thus not usable by companies selling commercial libraries.
- fpoling 9y ago
  Static checker can work in principle on binary code. Alternatively, one can annotate API the library provides for the static checker. This is especially feasible with C where API types and usage is typically rather simple. Clearly, this implies trusting API to be implemented correctly or at least using the static checker to prove that memory-safety bugs are originated in the library, not in the application code.
- jcelerier 9y ago
  That's not really relevant when talking about the linux kernel, though, is it ? There's tons and tons of open-source code that could just run clang-analyze today and eliminate swathes of memory bugs.
  - pjmlp 9y ago
    Sure it is, starting by the GPU drivers.
pcwalton 9y ago
I read the Cyclone papers when I designed the original Rust borrow checker, and we spoke to Dan Grossman. Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects. This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.

pjmlp 9y ago

Only works if 100% of the code is available, thus not usable by companies selling commercial libraries.

fpoling 9y ago
Static checker can work in principle on binary code. Alternatively, one can annotate API the library provides for the static checker. This is especially feasible with C where API types and usage is typically rather simple. Clearly, this implies trusting API to be implemented correctly or at least using the static checker to prove that memory-safety bugs are originated in the library, not in the application code.
jcelerier 9y ago
That's not really relevant when talking about the linux kernel, though, is it ? There's tons and tons of open-source code that could just run clang-analyze today and eliminate swathes of memory bugs.
- pjmlp 9y ago
  Sure it is, starting by the GPU drivers.

pcwalton 9y ago

I read the Cyclone papers when I designed the original Rust borrow checker, and we spoke to Dan Grossman. Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects. This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.