Stream: t-lang/wg-unsafe-code-guidelines

Topic: Gauging sanity of project idea

Shnatsel (Feb 10 2020 at 00:20, on Zulip):

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?

RalfJ (Feb 10 2020 at 17:57, on Zulip):

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

nikomatsakis (Feb 14 2020 at 16:43, on Zulip):

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., NotNull(x), where 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:

The whole idea is just to track "what are the things I think I thought about".

Elichai Turkel (Feb 16 2020 at 09:22, on Zulip):

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

RalfJ (Feb 16 2020 at 17:19, on Zulip):

@nikomatsakis yeah that sounds like an awesome tool indeed :D

lqd (Feb 17 2020 at 21:25, on Zulip):

maybe some of these use-cases could be modeled with mirai since it seems to handle some form of pre/post conditions/invariants contracts

Last update: Jun 07 2020 at 10:35UTC