Result declares a type-level invariant — an assertion enforced by the compiler, not runtime — that the operation can fail.
Ignoring that is bypassing the type system. It means your types are either wrong, or your type system is incapable of modeling your true invariants.
In the case of the cloudflare error, their types were wrong. That was an avoidable failure. They needed to fix their type-level invariants, not yolo the issue with `.unwrap()`.
Your willful persistent lack of understanding doesn’t mean my philosophy is incoherent. Using `.unwrap()` is always an example of a failure to accurately model your invariants in the type system.
Your definition of "correct" is completely incoherent. Just because an invariant that could be modeled by a type system is not modeled by the type system in any given scenario does not make it incorrect.
You can't engage with my examples and you provide none of your own. So continuing discussion with you is a waste of time.
This is literally what “invariant” means, and what a type system is built to model.
Declaring an invariant in the type system that you then violate is not correct code. I truly can’t even begin to guess at why you’re so voracious in your defense of this particularly poor practice.
[edit]
HN rate limits kicking in, so here’s my reply. I work for a FAANG but I’m not going to say which one. You or a relative are, with almost 100% certainty, relying on code written to that philosophy, by me, daily and widely.
Show me code you've published that is used by real people in real systems that follows the philosophy you've espoused here. Otherwise I'm calling shenanigans.
You are unnecessarily combative in this thread. I don't know what about the GP it is that ticks you off but they're making a lot of sense to me and I don't see why you would be loudly demanding published code when you are having a conversation about an abstract device.
If you haven't read my blog on this topic, I suggest you do so before replying further: https://burntsushi.net/unwrap
It should very clearly state my position. And it provides the examples that I previously referenced.
The GP got a link to this blog in the previous HN thread. They dismissed it out-of-hand without engaging with it at all. And tossed in an ad hominem for good measure. So your issue with me specifically here seems completely inappropriate.
I've presented examples. They haven't. They haven't even bothered to engage with the examples I've provided. I want to read code they've written using this philosophy so that I can see what it looks like in real world usage. Otherwise, the only code I've seen that does something similar uses formal methods. So I simply do not believe that this is practical advice for most programming.
Insisting on examples and evidence to support an argument isn't combative. It's appropriate when extraordinary claims are being made.
If you've published code using this philosophy that is used by real people in real systems, then I would be happy to take a look at that as well. If it exists, I would bet it's in a niche of a niche.
I've had these arguments before about this very topic. Some people have taken me up on this request and actually provided examples. And in 100% of those cases, it turned out there was a mismatch between what they were saying and what the code was doing.
> I work for a FAANG but I’m not going to say which one. You or a relative are, with almost 100% certainty, relying on code written to that philosophy, by me, daily and widely.
Cool story bro.
Like, even interpreted maximally charitably, your statement still doesn’t provide GP’s requested published code. Not “take my word for it” ostensibly deployed software—code; the discussion here is about code constructs for modeling invariants, not solely about runtime behavior.
I’d be interested to see that code discussed in context of the blog post GP linked, which seems to make a compelling argument.
I am enjoined from providing that, and it’d be idiotic to risk my career for an HN ****-measuring contest. If one can’t understand these concepts without example code then this probably isn’t a discussion one can meaningfully contribute to.
Not being able to envision how it is in fact possible to write code with these invariants encoded in the type system is a fundamental fault in one’s ability to reason about this topic, and software correctness in general, in the first place.
> Not being able to envision how it is in fact possible to write code with these invariants encoded in the type system is a fundamental fault in one’s ability to reason about this topic, and software correctness in general, in the first place.
Code proving that it’s possible to avoid branching into an abort (the concept, not necessarily the syscall) was not what the original GP requested. Nor was a copy of your employer’s IP. Published examples which demonstrate how real-world code which intentionally calls panic() could be better written otherwise was my interpretation of the request.
And I’m requesting that, too, because I am interested in learning more about it! Please don’t assume I’m asking out of inexperience with safety critical systems, dick-measuring, faulty reasoning ability, or unfamiliarity with using type systems to avoid runtime errors (where—and this is the source of this discussion—practical and appropriate). If you work on your tone, that would make it much easier to have educating discussions in contexts like this.
> 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?
They aren't presenting a coherent philosophy. And when asked for examples, or to engage directly with examples in my blog, they can't or won't do it.
But yes, of course it's okay to use unwrap(). It's just an assertion. Assertions are fine.