Rust can go that fast because of guarantees its compiler enforces about what the code is doing, that JS emphatically doesn't.
By all means build your tooling and runtime in Rust if it helps, but "you can write high-performance code in JS with no Rust-like constraints" is fundamentally a nonsense pitch.
I disagree. Right now, feedback on correctness is a major practical limitation on the usefulness of AI coding agents. They can fix compile errors on their own, they can _sometimes_ fix test errors on their own, but fixing functionality / architecture errors takes human intervention. Formal verification basically turns (a subset of) functionality errors into compile errors, making the feedback loop much stronger. "Come up with what software we need better than us in the first place" is much higher on the ladder than that.
TL;DR: We don't need to be radically agnostic about the capabilities of AI-- we have enough experience already with the software value chain (with and without AI) for formal verification to be an appealing next step, for the reasons this author lays out.
I completely agree it's appealing, I just don't see a reason to assume that an agent will be able to succeed at it and at the same time fail at other things that could make the whole exercise redundant. In other words, I also want agents to be able to consistently prove software correct, but if they're actually able to accomplish that, then they could just as likely be able to do everything else in the production of that software (including gathering requirements and writing the spec) without me in the loop.
> I also want agents to be able to consistently prove software correct...
I know this is just an imprecision of language thing but they aren't 'proving' the software is correct but writing the proofs instead of C++ (or whatever).
I had a but of a discussion with one of them about this a while ago to determine the viability of having one generate the proofs and use those to generate the actual code, just another abstraction over the compiler. The main takeaway I got from that (which may or may not be the way to do) is to use the 'result' to do differential testing or to generate the test suite but that was (maybe, don't remember) in the context of proving existing software was correct.
I mean, if they get to the point where they can prove an entire codebase is correct just in their robot brains I think we'll probably have a lot bigger things to worry about...
It's getting better every day, though, at "closing the loop."
When I recently booted up Google Antigravity and had it make a change to a backend routine for a web site, I was quite surprised when it opened Chrome, navigated to the page, and started trying out the changes to see if they had worked. It was janky as hell, but a year from now it won't be.
Aside from just being immensely satisfying, these patterns of defensive programming may be a big part of how we get to quality GAI-written code at scale. Clippy (and the Rust compiler proper) can provide so much of the concrete iterative feedback an agent needs to stay on track and not gloss over mistakes.
Nah, it reads like the normal logic behind the consulting model for open source monetization, except that Bun was able to make it work with just one customer. Good for them, though it comes with some risks, especially when structured as an acquisition.
The unwrap: not great, but understandable. Better to silently run with a partial config while paging oncall on some other channel, but that's a lot of engineering for a case that apparently is supposed to be "can't happen".
The lack of canary: cause for concern, but I more or less believe Cloudflare when they say this is unavoidable given the use case. Good reason to be extra careful though, which in some ways they weren't.
The slowness to root cause: sheer bad luck, with the status page down and Azure's DDoS yesterday all over the news.
The broken SQL: this is the one that I'd be up in arms about if I worked for Cloudflare. For a system with the power to roll out config to ~all of prod at once while bypassing a lot of the usual change tracking, having this escape testing and review is a major miss.
IMO: there should be explicit error path for invalid configuration, so the program would abort with specific exit code and/or message. And there should be a superviser which would detect this behaviour, rollback old working config and wait for few minutes before trying to apply new config again (of course with corresponding alerts).
So basically bad config should be explicitly processed and handled by rolling back to known working config.
You don’t even need all the ceremony. If the config gets updated every 5 minutes, it surely is being hot-reloaded. If that’s the case, the old config is already in memory when the new config is being parsed. If that’s the case, parsing shouldn’t have panicked, but logged a warning, and carried on with the old config that must already be in memory.
> If that’s the case, the old config is already in memory when the new config is being parsed
I think that's explicitly a non-goal. My understanding is that Cloudflare prefers fail safe (blocking legitimate traffic) over fail open (allowing harmful traffic).
System outputting the configuration file failed (it could check the size and/or content and stop right away), but also a system importing the file failed. These usually sound simple/stupid in a hindsight. I am not a fan of everything centralising to a few hands. As in bad situation, they can also be weaponised or attacked. And in good situation their blast radius is just too big and a bit random, in this case global.
The query is surely faulty: Even if this wasn’t a huge distributed database with who-knows-what schemas and use cases, looking up a specific table by its unqualified name is sloppy.
But the architectural assumption that the bot file build logic can safely obtain this operationally critical list of features from derivative database metadata vs. a SSOT seems like a bigger problem to me.
It's probably not ok to silently run with a partial config, which could have undefined semantics. An old but complete config is probably ok (or, the system should be designed to be safe to run in this state).
Even if you want it to crash, you almost never unwrap. At the very least you would use .expect() so you get a reasonable error message -- or even better you handle the potential error.
This wasn't a runtime property that could not be validated at compile time. And you don't need to fall back on "OS level security and reliability" when your type system is enforcing an application-level invariants.
In fact I'd argue that crashing is bad. It means you failed to properly enumerate and express your invariants, hit an unanticipated state, and thus had to fail in a way that requires you to give up and fall back on the OS to clean up your process state.
[edit]
Sigh, HN and its "you're posting too much". Here's my reply:
> Why? The end user result is a safe restart and the developer fixes the error.
Look at the thread your commenting on. The end result was a massive world-wide outage.
> That’s what it’s there for. Why is it bad to use its reliable error detection and recovery mechanism?
Because you don't have to crash at all.
> We don’t want to enumerate all possible paths. We want to limit them.
That's the exact same thing. Anything not "limited" is a possible path.
> If my program requires a config file to run, crash as soon as it can’t load the config file. There is nothing useful I can do (assuming that’s true).
Of course there's something useful you can do. In this particular case, the useful thing to do would have been to fall back on the previous valid configuration. And if that failed, the useful thing to do would be to log an informative, useful error so that nobody has to spend four hours during a worldwide outage to figure out what was going wrong.
The world wide outage was actually caused by deploying several incorrect programs in an incorrect system.
The root one was actually a bad query as outlined in the article.
Let’s get philosophical for a second. Programs WILL be written incorrectly - you will deploy to production something that can’t possibly work.
What should you do with a program that can’t work? Pretend this can’t happen? Or let you know so you can fix it?
> Programs WILL be written incorrectly - you will deploy to production something that can’t possibly work. What should you do with a program that can’t work? Pretend this can’t happen? Or let you know so you can fix it?
Type systems provide compile time guarantees of correctness such that systems cannot fail in ways covered by the type system.
In this case, they used an unsound hole in the type system to do something that unnecessarily abandoned those compile-time invariants and in the process caused a world-wide outage.
The answer is not to embrace poking unsound holes in your type system in the first place.
It's not philosophical, half of the internet broke. There is a notion between "I really have no other choice but to crash" and "I might wanna crash at this moment because something is wrong but I won't and I'll try recovering".
In this particular case, it was the "limit 200" because "performance reasons" so I think there was more space to implement the latter than the former.
The nice thing about the data center water usage panic is that whenever someone appeals to it, I immediately know that either they haven't done their homework or they're arguing in bad faith.
Rust can go that fast because of guarantees its compiler enforces about what the code is doing, that JS emphatically doesn't.
By all means build your tooling and runtime in Rust if it helps, but "you can write high-performance code in JS with no Rust-like constraints" is fundamentally a nonsense pitch.
reply