Live data from Hacker News

Cloudflare outage should not have happened

ebellani.github.io

221–230 of 265 posts

Re: Cloudflare outage should not have happened

#221

Earlier quoted context omitted.

Invariants aren’t invariant if they’re variant. 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…

> 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 mo…

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.

Re: Cloudflare outage should not have happened

#223

Earlier quoted context omitted.

I already had a conversation with the GP specifically: https://news.ycombinator.com/item?id=45979127 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.

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…

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

Re: Cloudflare outage should not have happened

#224

Earlier quoted context omitted.

> 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 mo…

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 t…

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

Re: Cloudflare outage should not have happened

#225

Earlier quoted context omitted.

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…

> 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 n…

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

Re: Cloudflare outage should not have happened

#226

Earlier quoted context omitted.

> 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 n…

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

Re: Cloudflare outage should not have happened

#227
post #180

Earlier quoted context omitted.

Was it a memory error or a data race? No. Rust only promises that those won't happen in safe Rust. What is embarrassing is trying to pin this on a specific programming language.

[flagged]

This has nothing to do with the language, and it's so irritating to see people falsely claiming it is. There is nothing whatsoever about Rust that meant the engineer had to write code to the effect of

  if result.is_err() {
    panic!()
  }
That was a choice on the engineer's part, not something caused by the language. You could choose to write that code in any language. It might even be the right choice sometimes! But whether or not it was the right choice, the fact remains that responsibility stops with the programmer(s) who decided to have that code, not somehow with the language.

Re: Cloudflare outage should not have happened

#228
post #71

Earlier quoted context omitted.

Agreed. I left out any commentary on `.unwrap()` from my original comment, but it’s an obvious example of something that should never have appeared in critical code.

Rust needs to get rid of .unwrap() and its kin. They're from pre-1.0 Rust, before many of the type system features and error handling syntax sugar were added. There's no reason to use them as the language provides lots of safer alternatives. If you do want to trigger a panic, you can, but I'd also ask - why? Alternatively, and perhaps even better, Rust needs a way to mark functions that can panic for any reason other…

Unwrap is not only fine, it's a valuable part of the language. Getting rid of it would be a horrible change. What needs to happen is not using an assert (which is really what unwrap is) if an application can't afford to crash.

Re: Cloudflare outage should not have happened

#229

Earlier quoted context omitted.

> 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 n…

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

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?

Re: Cloudflare outage should not have happened

#230
post #109

Earlier quoted context omitted.

It is the aggregate they pay that counts here, not the individual payments. A better comparison would be to compare this to airline passengers paying for their tickets, they pay a few hundred bucks in the expectation that they will arrive at their destination. Besides, it is not the customers that determine Cloudflare's business model, Cloudflare does. Note that their whole business is to prevent outages and that as…

> as soon as they become the cause of an outage they have invalidated their whole reason for existence This is a bar no engineering effort has ever met. “If you ever fail, even for a moment, there’s no reason for you to even exist.” There have been 6 fatal passenger airplane crashes in the US this year alone. NASA only built 6 shuttles and 2 of those exploded, killing their crews. And these were life-preserving syste…

The NASA example should highlight the normalisation of deviance. The Challenger o-rings had failed before and while engineers were very vocal about that, management overruled them. The foam impacts and tile loss were also a known factor in the Columbia disaster but the abort window is very small. Both point to perverse incentives: maintaining the gravy train. One comment made the point earlier that if Cloudflare were more thorough they would not have captured the market because they would be slower. Slow is smooth and smooth is fast but YMMV. At the end of the day everything can be tracked down to a system that incentivizes wealth accumulation over capability with the fixation that capability can be bought which is a lie.
Post reply on HN