3 ms·

This is not fighting the compiler, this is writing code in a way which can be proved to be safe. Some code can be safe but is hard to reason about. The compile

by baq 3y ago

This is not fighting the compiler, this is writing code in a way which can be proved to be safe. Some code can be safe but is hard to reason about. The compiler tells you that. The solution is, unsurprisingly but perhaps disappointingly, to stop writing code like that.

Animats 3y ago
> Some code can be safe but is hard to reason about. This is a point I made back when I was doing verification. Yes, you can write code for which termination cannot be proven. If termination for your code is theoretically undecidable, it probably won't work right anyway. So don't go there. Microsoft took a hard line on this with their Static Driver Verifier, a proof of memory correctness system for Windows kernel drivers. If your driver code is so hard to analyze that automatic path analysis can't verify memory correctness, it doesn't get signed to run in kernel space. Driver-caused Windows kernel crashes, formerly a huge problem, mostly went away.
kramerger 3y ago
What you basically wrote is that my problems would go away if only I wrote code that the compiler approves.. But that is not easy, and much of that is due to the complexity of Rust and the way it handles memory safety. Which is where fighting the compiler comes in.
- baq 3y ago
  Yeah I get it, I was there. It is super hard if you actually know C/C++ or mastered a GC language. Rust won’t like some patterns at all and will fight you. The point is, there are replacements for those patterns that are safer, about as performant and simultaneously easier to reason about by both you and the compiler. To stop fighting, you must switch to them. Old ways will not work. This is by design and a key point of Rust. A single, concrete example: do not use references in object graphs. Use an array and indexes into it. If you have a dynamic structure with many additions and deletions, use generational indexing.

by baq 3y ago

Animats 3y ago

> Some code can be safe but is hard to reason about. This is a point I made back when I was doing verification. Yes, you can write code for which termination cannot be proven. If termination for your code is theoretically undecidable, it probably won't work right anyway. So don't go there. Microsoft took a hard line on this with their Static Driver Verifier, a proof of memory correctness system for Windows kernel drivers. If your driver code is so hard to analyze that automatic path analysis can't verify memory correctness, it doesn't get signed to run in kernel space. Driver-caused Windows kernel crashes, formerly a huge problem, mostly went away.

kramerger 3y ago

What you basically wrote is that my problems would go away if only I wrote code that the compiler approves.. But that is not easy, and much of that is due to the complexity of Rust and the way it handles memory safety. Which is where fighting the compiler comes in.

baq 3y ago
Yeah I get it, I was there. It is super hard if you actually know C/C++ or mastered a GC language. Rust won’t like some patterns at all and will fight you. The point is, there are replacements for those patterns that are safer, about as performant and simultaneously easier to reason about by both you and the compiler. To stop fighting, you must switch to them. Old ways will not work. This is by design and a key point of Rust. A single, concrete example: do not use references in object graphs. Use an array and indexes into it. If you have a dynamic structure with many additions and deletions, use generational indexing.