Announcing pre, a crate to offer compile-time assistance for working with unsafe code

[aticu]

pre is a library that helps you keep tabs on what exactly needs to be true in order for unsafe code to be safe.

You can think of it essentially like a Safety comment at the definition and call site, except that the compiler checks that the comments actually talk about the same thing.
This does not incur any cost at runtime in a release build.

It works by annotating functions with preconditions that need to be upheld when calling them.
These preconditions are transformed into an additional (zero-sized) argument to the function.
Callers then have to assure that the preconditions are upheld. Those assurances make up the additional argument at the call site and must match the original preconditions in order for the argument to type-check.
This avoids missing any changes in the safety requirements later. So it is most useful in larger projects with multiple people or for library authors, who want to make their preconditions part of the API.
The burden of proof still lies with the programmer however.

You can also think of it as a combination of the safety-guard crate and the safe crate.

Example

Suppose you have this code:

fn init_foo() {
    /* ... */
}

/// # Safety
/// 
/// `init_foo` must be called before you can call `use_foo`.
unsafe fn use_foo() {
    /* ... */
}

fn main() {
    init_foo();

    unsafe {
        // Safety: This is safe, because `init_foo` was called first.
        use_foo();
    }
}

Using pre, it could be rewritten into this code:

fn init_foo() {
    /* ... */
}

use pre::pre;

#[pre("is only called after `init_foo` was called")]
unsafe fn use_foo() {
    /* ... */
}

#[pre]
fn main() {
    init_foo();

    unsafe {
        #[assure(
            "is only called after `init_foo` was called",
            reason = "`init_foo` was called first"
        )]
        use_foo();
    }
}

Now if someone who isn't aware of the relationship between the two functions writes this code somewhere else:

use pre::pre;

#[pre]
fn not_main() {
    unsafe {
        use_foo(); // Oops, didn't call `init_foo` first
    }
}

The code will fail to compile:

error[E0061]: this function takes 1 argument but 0 arguments were supplied
  --> src/main.rs:28:9
   |
7  |   #[pre("is only called after `init_foo` was called")]
   |  _______-
8  | | unsafe fn use_foo() {
9  | |     /* ... */
10 | | }
   | |_- defined here
...
28 |           use_foo(); // Oops, didn't call `init_foo` first
   |           ^^^^^^^-- supplied 0 arguments
   |           |
   |           expected 1 argument

The error message is not the most readable one, but I think it's better to spend a little time to understand an error than it is to have bugs in my program.

Background

I'm writing this library for my bachelor's thesis and I'd be very happy if you could give me feedback about it.

Would you use it? If not, why not?

Feel free to give it a try and let me know how it went.

Also if you are an author of a crate that might benefit from something like this, but don't have the time to integrate it yourself, feel free to contact me.