> Result declares a type-level invariant — an assertion enforced by the compiler, not runtime — that the operation can fail.
“Can do X” is not an invariant. “Will never do X” (or “Will always do Y”) is an invariant. “Can do X” is the absence of the invariant “Will never do X”.
> Using `.unwrap()` is always an example of a failure to accurately model your invariants in the type system.
No, using .unwrap() provides a narrower invariant to subsequent code by choosing to crash the process via a panic if the Result contains an Error.
It may be a poor choice in some circumstances, and it may be a result of mistakenly believing that code returning the Result itself had failed to represent its invariants fully such that the .unwrap() would be a noop—but even there it respects and narrows the invariant declared, it doesn't ignore it—and, in any case, as it has well-defined behavior in either of the possible input cases, it is silly to describe using it as a failure accurately model invariants in the type system.
“Narrowing” a compile-time invariant without a corresponding proof is formally unsound and does not “respect” the declared invariant in any reasonable sense.
What’s silly is the desire to pretend otherwise because it’s easier.
> “Narrowing” a compile-time invariant without a corresponding proof is formally unsound and does not “respect” the declared invariant in any reasonable sense
The invariant is that either condition X applies or condition Y applies. "Panic and stop execution if X, continue execution with the invariant Y if Y" is not unsound and does respect the original invariant in every possible sense.
It may be the wrong choice of behavior given the frequency of X occurring and the costs incurred by the decision to panic, but that’s not a type-level problem.
Formal verification is well and good, but that is not what unsoundness means.
If a proof trivially demonstrated that a given program’s behavior was indeed “proceed if a condition is satisfied, crash otherwise”, then what? Or do we not trust the verifier with branching code all of a sudden?
“Can do X” is not an invariant. “Will never do X” (or “Will always do Y”) is an invariant. “Can do X” is the absence of the invariant “Will never do X”.
> Using `.unwrap()` is always an example of a failure to accurately model your invariants in the type system.
No, using .unwrap() provides a narrower invariant to subsequent code by choosing to crash the process via a panic if the Result contains an Error.
It may be a poor choice in some circumstances, and it may be a result of mistakenly believing that code returning the Result itself had failed to represent its invariants fully such that the .unwrap() would be a noop—but even there it respects and narrows the invariant declared, it doesn't ignore it—and, in any case, as it has well-defined behavior in either of the possible input cases, it is silly to describe using it as a failure accurately model invariants in the type system.