bytes icon indicating copy to clipboard operation
bytes copied to clipboard

Safety documentation

Open aticu opened this issue 4 years ago • 0 comments

I've developed a library for my bachelor's thesis to make working with unsafe code a little bit safer.

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 bytes. If so, which part of the code do you think 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.

aticu avatar Jul 22 '20 21:07 aticu