Should we try to be more formal about safety?

[llogiq]

e.g. I could envision a fn upholds_invariants() -> bool method that could be debug_assert!ed on all methods that use unsafe, thereby allowing us to fuzz-check for mistakes we may have made w.r.t. memory safety. Alas, there are some invariants we cannot check for now (namely around uninitialized memory), but we could at least document them.

We could also add more comments describing why what we do really should be safe, so others can understand – and try to poke holes into – our thinking.

[dpc]

I was just filling a cargo-crev advisory, following RustSec one, and I've noticed that a while ago I was briefly reviewing this crate and what was striking to me, that it is in dear need of fuzzing

You could follow examples from eg. rust-bitcoin project fuzzing.

[Shnatsel]

https://github.com/jakubadamw/arbitrary-model-tests should make fuzzing a breeze, since you already have std::vec as a model to check against.

[aticu]

I've developed a library for my bachelor's thesis which has the goal to aid developers in being more formal about safety.

It works by annotating unsafe functions with the preconditions that need to be upheld for their safety.
A call to an annotated function will fail to compile, unless it is assured at the call site that the preconditions hold.
Assuring this uses another annotation at the call site.

This has two main advantages:

• It is documented in the code why a piece of unsafe code is safe.
• This documentation is partially checked by the compiler. If the conditions that need to be upheld change, it can be noticed right away.

Such annotations could be added behind a cfg as a dev-dependency or also - optionally - behind a feature flag as part of the public API for the unsafe functions.

If you'd be interested in such annotations, I would be happy to prepare a pull request adding some of them to smallvec. If so, which part of the code would benefit most from such annotations?

If you're not interested, I'd appreciate it, if you could briefly let me know why, as that would be valuable feedback for my thesis.

[Shnatsel]

Meanwhile arbitrary-model-tests was renamed to rutenspitz and since yesterday correctly handles panics. It should make fuzzing very easy, and also easily allow verifying that behavior of SmallVec is identical to that of Vec.