> I disagree. I learnt good stuff from this article and it’s enough.
That's perfectly fine. It's also besides the point though. You can learn without reading random people online cynically shit talking others as a self promotion strategy. This is junior dev energy manifesting junior level understanding of the whole problem domain.
There's not a lot to learn from claims that boil down to "don't have bugs".
Not to single you out in particular, but I see this sentiment among programmers a lot and to me it's akin to a structural engineer saying "I laughed out loud when he said they should analyze the forces in the bridge".
Care to elaborate? Perhaps the tools to do this in practice aren't there (which just shows how young the field of software "engineering" really is), but what consensus are you talking about and how is it an obstacle to verifying code? Most of the web follows standards and protocols, which actually sort of a prerequisite for communications across different systems...
Basically the modern web uses orchestration, for pretty much everything. Usually Kubernetes is doing that. Theoretically protocols like RAFT are formally verifiable, but their implementations in orchestration tools like etcd have not been, and I would go so far as to say that that is an impossible task. Therefore, the entire exercise is kind of silly.
Thanks, interesting. However, that just seems like a protocol like any other, with no real reason why you "can't" formally verify it. Is there something special about a consensus algorithm / protocol that makes it any more difficult to verify than any other algorithm which doesn't yet have a formally verified implementation?
> You can't formally verify anything that uses consensus
What did you mean by this then? There certainly seems to be nothing special about consensus that makes it any harder to verify than anything else. It's not fundamentally impossible to verify the software that CERN uses, it just takes some work.
A bridge failing is a high likelihood of death or serious injury. How many people died or were seriously injured in the latest Cloudflare outage?
For life or death systems, I agree that we should be looking to implement analogous processes/systems to a structural engineer or doctor, etc. Cloudflare is not a life or death system. If you operate a life or death system and you have Cloudflare as a single point of failure, for some reason, that should not be Cloudflare's problem.
> How many people died or were seriously injured in the latest Cloudflare outage?
I would not be surprised if the answer is "several". The average impact per human is obviously pretty small, but across billions of humans, there will be outliers.
Maybe a fire department uses a coordination system that relies on cloudflare, and with cloudflare down they have to resort to their backup system, and their backup system works but is slightly worse and causes one engine to be delayed in their response, and because they're 3 minutes late, they just miss being able to save someone from the fire.
Maybe someone's running a scientific study on nutrition, and the cloudflare outage means their data collection system is goes down for a bit, so their data flawed, and they end up just barely not passing a some necessary threshold, and they have to rerun their study, and that takes an extra week, and then they miss that quarter's deadline, and then the resulting adjustment to a product/procedure is delayed, and that 3 month delay causes 100,000 people to be slightly more malnourished than they would be otherwise, and one of those people ends up just barely too unhealthy to survive an unrelated deadly illness.
Sure, these scenarios are far-fetched. The chance of if it happening is one-in-a-million.
There are 10000 one-in-a-million people on the earth.
Sure, but this sentiment is why software "engineering" isn't really. You can justify it by not being important enough for actual engineering practices I guess, but to me it's a lack of pride in and care of your product.
more like "I laughed out loud when he said they should FEM the whole structure, down to the last bolt and strand of cable".
(More seriously, 'formal verification' is not a single thing, more a class of techniques which allow you to statically guarantee some properties of the system you are working with. When you propose it, you should have a clear idea of what properties you care about and how you intend to prove them, as well as a strong concern about whether those properties are actually going to capture enough of what you care about for it to be worthwhile)
This article actually explains how this bug in particular could have been avoided. Sure you may not consider his approach realistic, but it's not at all saying "don't have bugs". In fact, not having formal verification or similar tooling in place, would be more like saying "just don't write buggy code".
> This article actually explains how this bug in particular could have been avoided.
Not really. The article is a textbook example of hindsight bias. It's a simplistic analysis of a far more complex problem that goes over the blogger's head, and results in a string of simplistic assertions that fail to address any of the issues. Read up on the definition of monday morning quarterback.
Not commenting on the quality of this post but occasional writing that responds to an event provides a good opportunity to share thoughts that wouldn’t otherwise reach an audience. If you post advice without a concrete scenario you’re responding to, it’s both less tangible for your audience and less likely to find an audience when it’s easier to shrug off (or put off).
That's perfectly fine. It's also besides the point though. You can learn without reading random people online cynically shit talking others as a self promotion strategy. This is junior dev energy manifesting junior level understanding of the whole problem domain.
There's not a lot to learn from claims that boil down to "don't have bugs".