As of now there exists only 1 lint that checks usage of pub unsafe and does not distinguish between 1. callee and 2. caller.
But the callee defines assumptions for the implementor, whereas the caller a justification that the assumption is fullfilled (for reviewers). Reformulating the underlying formal models informally: The callee defines the potential domains of inputs informally, whereas the caller picks one (hopefully correct) and we need to reason about this relation on code review.
Also the annotation Safety feels redundant to the annotation unsafe, whereas the actual meaning is this function has the following assumption or assume: condition holds for logical correctness.
Thus I suggested to use assume: to annotate unsafe macro/trait/fn (callee) and safety: for unsafe blocks in the book, which suggested this is the place to discuss or decide on this.
Further I find it disappointing to make safety reasoning only for public interfaces and clutter it in the lint with a whitespace,
whereas developers that change code semantics prefer having related things as closely together as possible.
This may be good for a book format and rarely changing public interfaces, but work worse for more frequent changing code.
Additionally, explaining code semantics and supporting via lint is a very good idea overall to increase code and developer quality.
Would you be interested in a PR changing all usage unsafe accordingly or what argument do you have for not doing that as part of best practice?
As of now there exists only 1 lint that checks usage of
pub unsafeand does not distinguish between 1. callee and 2. caller.But the callee defines assumptions for the implementor, whereas the caller a justification that the assumption is fullfilled (for reviewers). Reformulating the underlying formal models informally: The callee defines the potential domains of inputs informally, whereas the caller picks one (hopefully correct) and we need to reason about this relation on code review.
Also the annotation
Safetyfeels redundant to the annotationunsafe, whereas the actual meaning is this function has the followingassumptionorassume: condition holdsfor logical correctness. Thus I suggested to useassume:to annotateunsafe macro/trait/fn(callee) andsafety:forunsafeblocks in the book, which suggested this is the place to discuss or decide on this.Further I find it disappointing to make safety reasoning only for public interfaces and clutter it in the lint with a whitespace, whereas developers that change code semantics prefer having related things as closely together as possible. This may be good for a book format and rarely changing public interfaces, but work worse for more frequent changing code.
Additionally, explaining code semantics and supporting via lint is a very good idea overall to increase code and developer quality.
Would you be interested in a PR changing all usage
unsafeaccordingly or what argument do you have for not doing that as part of best practice?