ralfj

11 ms·

1. 91.▲
   by ralfj 11y ago

   I suggested something kind-of-similar at < https://internals.rust-lang.org/t/pre-rfc-unsafe-types/3073>
2. 92.▲
   by ralfj 11y ago

   To reach a conclusion here, we will have to agree on what it means to be the "cause of the problem". It is true that if a program crashes, then there has to be some unsafe code in that program. This statement is however not very
3. 93.▲
   by ralfj 11y ago

   This is not a counter-example to the claim you are citing. If you added this form of `evil` to `Vec`, then since `evil` is within the module, the proof of correctness has to cover `evil`. Doing that proof will fail. So, it is not necessary
4. 94.▲
   by ralfj 11y ago

   Since Rust supports concurrency, it is worth mentioning that these techniques have been scaled to handle objects that can be accessed from multiple threads at once - while maintaining the modularity of the approach. See, for example, < h
5. 95.▲
   by ralfj 11y ago

   One of the fundamental differences is that in Rust, you only have to prove correct every module that contains unsafe code, and the proof then automatically expands to your entire program. The experience in practice is that most module - t