This is mostly asking if this is the right way to go about this, the comments are nowhere near done.
The wording can be updated, but my main questions are
Would it be too verbose to add safety comments to all of the unsafe blocks here? I could instead have a chapter implementing something simpler. I'm expecting a few lines of docs above every unsafe block.
I sometimes need to call back to invariants on the type (i.e. pointer is either allocated or dangling). For now I think I'll not do anything about that, but in the future I might decide to copy paste the Vec's definition with all the invariants (or just copy paste the invariant text) whenever we use them.
Sometimes we can't actually prove safety of something because it was ignored for simplicity reasons. I don't actually remember which comments were like this, but I distinctly remember some safety being unprovable. Assuming this comes up, what should I do?
This is mostly asking if this is the right way to go about this, the comments are nowhere near done.
The wording can be updated, but my main questions are