DBdbaupp·Jan 11, 2016
I'm not really sure what the problem is here: having to formally verify a module doesn't seem fundamentally different to formally verify a single function. I mean, sure, it's some more code, but there's still well-defined containment. And, being "allowed" to reason about a whole module (well, usually one just cares about a whole type, but these often match, especially for unsafe code) seems far more useful: one can build far more interesting abstractions. If one was forced to reason about a single function at a time, Vec couldn't exist in a useful way, as every function would have to assume the incoming Vec value could be arbitrarily invalid.
In any case, there are many many modules with no `unsafe` code, e.g. std::option has none [1], iron::response has none [2], image::jpeg has none [3] (just some random examples). These are automatical
Read the rest
ly safe, if you assume that that the code they call is safe, which seems to me like the only assumption that can make sense: if the safe modules call unsafe ones that aren't safe... well, the problem is in the unsafe ones, not the safe ones.
What I'm trying to say is this paragraph doesn't seem to change anything fundamental about the objections to safe vs. unsafe you sometimes write about; it is not introducing anything new, and so the refutations you often receive still apply.
[1]: https://github.com/rust-lang/rust/blob/dfaddb732ced1da9d3109...
[2]: https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e...
[3]: https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c...