bkettle

Are you based in Alaska? I’d love to hear more if so; I have contact info on my website. (I grew up there).

Yeah fair enough. I can definitely see the value of property-based verification like this and agree that useful properties could be easy to express and that LLMs could feasibly verify them. I think full verification that an implementation implements an entire spec and nothing else seems much less practical even with AI, but of course that is just one flavor of verification.

The whole point I think, though, is that it doesn’t matter. If an LLM hallucinates a proof that passes the proof checker, it’s not a hallucination. Writing and inspecting the spec is unsolved, but for the actual proof checking hallucinations don’t matter at all.

I think formal verification shines in areas where implementation is much more complex than the spec, like when you’re writing incomprehensible bit-level optimizations in a cryptography implementation or compiler optimization phases. I’m not sure that most of us, day-to-day, write code (or have AI write code) that would benefit from formal verification, since to me it seems like high-level programming languages are already close to a specification language. I’m not sure how much easier to read a specification format that didn’t concern itself with implementation could be, especially when we currently use all kinds of frameworks and libraries that already abstract away implementation details.

Sure, formal verification might give stronger guarantees about various levels of the stack, but I don’t think most of us care about having such strong guarantees now and I don’t think AI really introduces a need for new guarantees at that level.

> there's a section of road near where I live that's dangerous, and we all know it's dangerous

Clearly not enough people know it’s dangerous or how dangerous it is, or one of them would do something about it

Semgrep has supported uv for months now (I added it).

This free tradition in software is I think one of the things that I love so much, but I don't see how it can continue with LLMs due to the extremely high training costs and the powerful hardware required for inference. It just seems like writing software will necessarily require paying rent to the LLM hosts to keep up. I guess it's possible that we'll figure out a way to do local inference in a way that is accessible to everyone in the way that most other modern software tools are, but the high training costs make that seem unlikely to me.

I also worry that as we rely on LLMs more and more, we will stop producing the kind of tutorials and other content aimed at beginners that makes it so easy to pick up programming the manual way.

I think they mean backwards-compatible syntax-wise, rather than actually allowing this feature to be used on existing code. If I’m understanding correctly they would prefer for the Python grammar to stay the same (hence the comment about updating parsers and IDEs).

But I don’t think I really agree, the extensible annotation syntaxes they mention always feel clunky and awkward to me. For a first-party language feature (especially used as often as this will be), I think dedicated syntax seems right.

I actually think that Cloudflare has made publishing on the internet _more_ accessible for many individuals. I’ve helped a few people get personal websites running on Cloudflare pages and run my own there—it’s free and extremely easy. They could obviously pull the plug at any point, but with static sites it’s easy to avoid lock-in. If it weren’t for Cloudflare and other services that give free, easy hosting, I suspect there would be even fewer of the non-commercial small-internet sites that you value.

Hm. To me it is indeed the big bad tech companies at fault for implementing _obviously_ user-hostile functionality (mandatory suggested posts, for example) that exploit human nature to keep people engaged, even if people prefer not to. The existence and widespread use of screen time limits on phones seems like strong evidence that tech companies have built something nefarious here. And to me, it’s clear that they have done so intentionally to drive profit.

Is it possible that the current form of social media is actually contributing to the erosion of your liberties because it is so widely used in society and is likely contributing to polarization and antisocial behavior?

I see this (and, honestly, most problems) as much more than a personal responsibility issue. To me, it’s an issue of misaligned incentives and unpriced downside costs. It’s clear that market forces push companies to build an addictive service that produces long term misery. It’s also clear that social media has a cost on its users (producing long term misery, reducing acute productivity) But this cost is not paid by the social media company.

I’d argue that widespread use of the social media that today’s market incentives create is bad for society as a whole, not only for any one individual. Correcting market incentives that don’t align with social good is, in my opinion, one of the most essential purposes of legislation.