Project idea: given a piece of unsafe code, make a list of all the invariants you need to uphold, so you can be sure you don't forget to check an invariant you need to uphold when looking at unsafe code. Inspired by The Checklist Manifesto.
e.g. if there is a raw pointer dereference => non-null, alignment, aliasing, provenance, in bounds, target is initialized (and I'm probably forgetting something)
Any thoughts on whether this is feasible or practical?
hm... sounds like an interesting experiment. we have some long-term plans to do that in a formal way (so, it would list all the coq proof obligations you have to show), but doing something that normal people can read would probably be more widely applicable :D
Related to something I've always wanted:
I've wanted wanted to be able to informally write the "things one must prove" in the form of prolog-like predicates. e.g.,
x is the name of a parameter or something, and then have a tool that lints that -- on the relevant unsafe block around a call
foo(y) -- I have written something like
// assert NotNull(y).
The idea here is:
Aligned(x), then I'll start to get lint errors at every call site until I added
// assert Aligned(y)to state that I believe it holds.
The whole idea is just to track "what are the things I think I thought about".
nikomatsakis This sounds pretty cool, because for me the hardest part is revisiting some unsafe code and modifying it but forgetting some weird invariant I added a while ago
@nikomatsakis yeah that sounds like an awesome tool indeed :D
maybe some of these use-cases could be modeled with
mirai since it seems to handle some form of pre/post conditions/invariants contracts