Bindings can leverage the ownership and borrowing principles in Rust to codify comments typically found in a C header about how its API should be used. Could t

Bindings can leverage the ownership and borrowing principles in Rust to codify comments typically found in a C header about how its API should be used. Could the Rust compiler make use of design by contract style annotations in the C header? Maybe it could reason that an unsafe block is in some ways safe. There is a specification language for C called ACSL (which was designed for and is mainly used by Frama-C). Annotations look like: /*@ ensures \result >= 0; assigns \nothing; */ int foo(int x) { if (x < 0) return 0; return x; } I noticed there are annotations for Rust with the LibHoare library (https://github.com/nrc/libhoare https://github.com/nrc/libhoare). The example above might look like: #[postcond="result >= 0"] fn foo(x: int) -> int { if x < 0 { 0 } else { x } } It would be really cool if ACSL could be translated to LibHoare.