> “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.

Claiming panic as sound and not a type-level problem is very cute, but also clearly wrong and a bit hilarious after the outage in question.

You guys really will go to any possible rhetorical length to justify lazy programming practices in error handling.

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?