I think that's right but also the "trust bootstrapping problem" is not a real problem in practice.

grind is already an SMT solver and is widely used in Lean; I think tools like that are going to be a big part future developments. The Bitter Lesson includes search for a reason.

Obviously you find and fix bugs when verifying, but there are a lot of bugs that need to be fixed first that fuzzing will find.

This isn't quite news, but Dukakis losing the kids vote at my elementary school.

Isn't the a big confound that companies using Ramp are way more likely to be VC backed?

"gradual typing"

But proving something much stronger, like "Chrome doesn't leak information from other origins to web pages" will require several more big steps forward.

The most exciting thing is the insight that we can go a long way with just that property -- it's the same insight that makes fuzz testing unreasonably effective, but lifted to formal verification. Probably there are a lot more wins in this direction.

1. Extending this to x86 is just "work", there's already semantics for x86 and Claude even wrote one in the post. 2. The limitation here is the property being verified. The big result here is proving that the program doesn't crash given some inputs, not that it works correctly.

The differences between what has been announced in terms of verification and in math, as well as the wildly different reactions from formal verification people compared to mathematicians, should tell you that this is not true at all.

Because (a) fuzzing is also 0 human effort and (b) proving that things are correct goes better after you remove the bugs.

Indeed. Wir mussen wissen!

I mean, I agree that we can't be sure what the models will be able to do in a couple years. But I think the trajectory of programming is more bullish for people than you're suggesting.

I think understanding means two different things here. Wanting to pay human mathematicians because we want humanity to understand math is different than wanting to pay Derek because understanding eventually leads to Iris.

Tell the robots that it renders wrong in Firefox on my phone.

We should ask @diagram_chaser

Are those last 3 really using it in the same sense? "Morally correct" is an idiom that did not originate in that paper.

Certainly what those students worry about is possible; I didn't think we would be here now already. But Anthropic and Theorem are using Verus and Rocq, they're using Arjun's semantics. And they aren't at the interesting properties of the application yet, even with a billion LoC.

I think Umang is basically right. The people who aren't excited are going to be people who are anti LLM on general principles, not people who were really looking forward to spending years verifying zlib on riscv.