Repository: rust-lang/rust
File: library/std/src/keyword_docs.rs (Rust)

Code before:
/// impl Indexable for ! {
///     const LEN: usize = 0;
///
///     /// See `Indexable` for the safety contract.
///     unsafe fn idx_unchecked(&self, idx: usize) -> i32 {
///         // SAFETY: As per this trait's documentation, the caller ensures
///         // that `idx < 0`, which is impossible, so this is dead code.
///         unsafe { std::hint::unreachable_unchecked() }
///     }
/// }
///
/// fn use_indexable<I: Indexable>(x: I, idx: usize) -> i32 {
///     if idx < I::LEN {
///         // SAFETY: We have checked that `idx < I::LEN`.
///         unsafe { x.idx_unchecked(idx) }
///     } else {
///         panic!("index out-of-bounds")
///     }
/// }
/// ```
///
/// This time, `use_indexable` is safe because it uses a run-time check to discharge the safety
/// contract of `idx_unchecked`. Implementing `Indexable` is safe because when writing
/// `idx_unchecked`, we don't have to worry: our *callers* need to discharge a proof obligation
/// (like `use_indexable` does), but the *implementation* of `get_unchecked` has no proof obligation
/// to contend with. Note that unlike normal `unsafe fn`, an `unsafe fn` in a trait implementation
/// does not get to just pick an arbitrary safety contract! It *has* to use the safety contract
/// defined by the trait (or a stronger contract, i.e., weaker preconditions).
///
/// Of course, the implementation may choose to call other unsafe operations, and then it needs an
/// `unsafe` *block* to indicate it discharged the proof obligations of its callees. (We enabled
/// `unsafe_op_in_unsafe_fn`, so the body of `idx_unchecked` is not implicitly an unsafe block.) For
/// that purpose it can make use of the contract that all its callers must uphold -- the fact that
/// `idx < LEN`.
///
/// Formally speaking, an `unsafe fn` in a trait is a function with *preconditions* that go beyond
/// those encoded by the argument types (such as `idx < LEN`), whereas an `unsafe trait` can declare
/// that some of its functions have *postconditions* that go beyond those encoded in the return type
/// (such as returning an even integer). If a trait needs a function with both extra precondition
/// and extra postcondition, then it needs an `unsafe fn` in an `unsafe trait`.
///
/// [`extern`]: keyword.extern.html
/// [`trait`]: keyword.trait.html
/// [`static`]: keyword.static.html
/// [`union`]: keyword.union.html
/// [`impl`]: keyword.impl.html
/// [raw pointers]: ../reference/types/pointer.html
/// [memory safety]: ../book/ch19-01-unsafe-rust.html
/// [Rustonomicon]: ../nomicon/index.html
/// [nomicon-soundness]: ../nomicon/safe-unsafe-meaning.html
/// [soundness]: https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#soundness-of-code--of-a-library

Review comment (suggestion):
> but the *implementation* of `get_unchecked` has no proof obligation to contend with.

I might suggest a parenthetical here that hints at what will follow in the next paragraph.  Almost always, such an implementation will have an `unsafe` block within.

Code after:
/// fn use_indexable<I: Indexable>(x: I, idx: usize) -> i32 {
///     if idx < I::LEN {
///         // SAFETY: We have checked that `idx < I::LEN`.
///         unsafe { x.idx_unchecked(idx) }
///     } else {
///         panic!("index out-of-bounds")
///     }
/// }
/// ```
///
/// This time, `use_indexable` is safe because it uses a run-time check to discharge the safety
/// contract of `idx_unchecked`. Implementing `Indexable` is safe because when writing
/// `idx_unchecked`, we don't have to worry: our *callers* need to discharge a proof obligation
/// (like `use_indexable` does), but the *implementation* of `get_unchecked` has no proof obligation
/// to contend with. Of course, the implementation may choose to call other unsafe operations, and
/// then it needs an `unsafe` *block* to indicate it discharged the proof obligations of its
/// callees. For that purpose it can make use of the contract that all its callers must uphold --
/// the fact that `idx < LEN`.
///
/// Note that unlike normal `unsafe fn`, an `unsafe fn` in a trait implementation does not get to
/// just pick an arbitrary safety contract! It *has* to use the safety contract defined by the trait
/// (or one with weaker preconditions).
///
/// Formally speaking, an `unsafe fn` in a trait is a function with *preconditions* that go beyond
/// those encoded by the argument types (such as `idx < LEN`), whereas an `unsafe trait` can declare
/// that some of its functions have *postconditions* that go beyond those encoded in the return type
/// (such as returning an even integer). If a trait needs a function with both extra precondition
/// and extra postcondition, then it needs an `unsafe fn` in an `unsafe trait`.
///
/// [`extern`]: keyword.extern.html
/// [`trait`]: keyword.trait.html
/// [`static`]: keyword.static.html
/// [`union`]: keyword.union.html
/// [`impl`]: keyword.impl.html
/// [raw pointers]: ../reference/types/pointer.html
/// [memory safety]: ../book/ch19-01-unsafe-rust.html
/// [Rustonomicon]: ../nomicon/index.html
/// [nomicon-soundness]: ../nomicon/safe-unsafe-meaning.html
/// [soundness]: https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#soundness-of-code--of-a-library
/// [Reference]: ../reference/unsafety.html
/// [discussion on Rust Internals]: https://internals.rust-lang.org/t/what-does-unsafe-mean/6696
mod unsafe_keyword {}

#[doc(keyword = "use")]
//
/// Import or rename items from other crates or modules, use values under ergonomic clones
/// semantic, or specify precise capturing with `use<..>`.
///
/// ## Importing items
///
/// The `use` keyword is employed to shorten the path required to refer to a module item.