Discussion about robust blocks

[ia0]

In https://internals.rust-lang.org/t/detect-and-fix-overscope-unsafe-block/21660/23 was suggested to have robust blocks that are the dual of unsafe blocks. In an unsafe block, one has to prove something (i.e. unsafe blocks are proof goals). In a robust block, one adds something to the proof context (i.e. robust blocks are proof hypotheses/facts).

[dlight]

Ok so taking the discussion here, which seems more on topic:

I really think that Rust should become a bit closer to theorem provers. You could see something like unsafe(something) { .. } to pair it up with robust(something) { .. } for example, though I'm not sure how rustc could make use of that.

And of course this all can be very verbose, and I'm not sure it's a good tradeoff. One thing I suggested was that trusted dependencies could be annotated in Cargo.toml so calls to it are auto-robust (like it is today).

[ia0]

I really think that Rust should become a bit closer to theorem provers.

I can sympathize with that, but this is going to be an uphill battle. I think it's more reasonable to just use third-party tools (like Prusti, Creusot, RefinedRust, etc). Maybe in 20 years, one of those will get enough adoption that it will get supported by the language. But in the meantime, I don't think we'll get more than a common specification language, if at all.

You could see something like unsafe(something) { .. } to pair it up with robust(something) { .. } for example

It's sadly more complicated than that. You can't just pair facts and goals. An unsafe block creates a goal that may need multiple facts (each from a robust block) to be solved. Also, it all depends on your goal. If it is to have tooling support for change detection in proofs, to simplify maintenance, then indeed you could have something like you describe where the unsafe block would list all robust blocks it uses in its proof. Then if a robust block is changed and the safety comment of each unsafe block pointing to that robust block was not updated, the CI could create a warning or fail.

And of course this all can be very verbose, and I'm not sure it's a good tradeoff.

It's not gonna be a one-size-fits-all situation anyway. So each crate author will make the trade-off decisions themselves. Currently, it means choosing which correctness assurance they want to use (nothing, tests, fuzzing, other dynamic tools, static tools, sound tools or complete tools, automated or manual tools, etc).

One thing I suggested was that trusted dependencies could be annotated in Cargo.toml so calls to it are auto-robust (like it is today).

I guess this could be something shared between crates with tools like cargo-vet.