LiamPowell

Related: https://killedbygoogle.com/

I wonder if humans would have spotted this one if no one knew a LLM wrote it. Obviously it's nearly impossible to test that though.

This seems so poorly thought out.

The first obvious question is "why do agents need their own Stack Overflow?" They can already read docs and code well. Why would they need a source of indirect and outdated information?

Then we have this verification system where you're just going to have the same model verifying the same code using the same method across a bunch of instances. What's even the point? You gain nothing from this.

There's also a massive signal-to-noise problem. Look through the posts and it's already littered with junk. How is an agent meant to find anything useful when it has to sift through all this? https://agents.stackoverflow.com/all

For some reason you're not allowed to include citations, they say the reader should have to search for them themselves, that's just ridiculous, especially when they claim this is meant to be "evidence-based": "Wanting to cite something off-network (a vendor doc, a blog post, a GitHub issue): don’t paste the link. Quote or paraphrase the relevant content directly in your post, and name the source in plain text (e.g. "the FastAPI docs say…"). A reader who needs to verify can search."

It looks a lot like Fusion, where Autodesk took all the passable UI and UX from Inventor and replaced it with absolute garbage.

> we now charge users for those blocked requests

I'm so tired of Anthropic's bullshit and I can't believe anyone is willing to support them when they take such user-hostile actions. There's no other industry where a provider can say "we're going to take this job" and then later say "we're not going to give you the deliverables because it might have some of our IP in it, you still have to pay for it though".

Everyone is mentioning crawlers, but wouldn't most traffic from a datacenter's ASN usually be bots just in general given that there's not many humans there to generate human traffic?

It seems fairly obvious that it's meant to be an analogy for ChatGPT only supporting textual outputs until now (disregarding that it had some limited capabilities to show static images).

It looks fine in sRGB, but I can see how it would be bad with the horrid default profiles that monitors ship with. Graphic designers should really be aware of that at this point.

> yet what drives them is not well understood

Presumably the fact that they're heavily trained to reply in this way? I don't know about the rest of the paper, but this part sticks out as a really odd claim unless I'm entirely misunderstanding this part.

When the lines in the ASCII charts don't even line up my immediate assumption is that the author didn't even bother to glance at it.

I suspect they're also losing a lot of university subscriptions after they started advertising how you can use their service to cheat. I don't know what they were thinking with that marketing campaign given that universities are probably one of their biggest market segments.

You know what I mean, there's no clever on-chain reward script.

There is no script.

I can't believe that statistic about 186 pickups per day, that would be every 5 minutes on average assuming 16 hours awake.

The problem with using subagents is that you often have to rewrite a chunk of a program in a more proof-friendly way, just saying "go prove this code, don't edit it" doesn't work. Maybe I'm underestimating how effectively subagents can communicate though and they'd be fine asking for changes.

You don't have to let the ATP do everything, you can speed it up immensely with well placed assertions where it struggles. Maybe a hybrid approach is best where we run ATPs with a very low timeout to get all the easy stuff and then have a LLM write a proof using the thereoms that the ATPs were able to prove.

I feel that that's the worst option because it only leaves people who have read it without the added context at the start. If someone convinces me that I'm wrong then I'm happy to do so though.

Yes, I used Bend as an example because it is recent and high profile, and I also wanted to present my issues with it. I did not mean to conflate it with the main idea I was trying to present to the degree that I obviously did after reading my own writing as a third party would (at least to the degree that it is possible to do so).

> you can use tools to automate the proof-work, as you said so yourself.

The language doesn't appear to be designed around supporting existing tools (either by exporting to Why3 or manually interfacing with existing tools). I'm not against shipping the whole proof or storing it on a cache server, I'm against the idea of having a LLM write it all. Even having the LLM only write proofs for subprograms that take a long time for ATPs to prove would work.

For the example in the article, the LLM had to write it exactly once without any iteration and it proved in a second, which I assume was mostly startup time. Having a LLM write 442 lines instead, which I assume also needed some iteration, is a tough sell in comparison.

ATPs go quite a bit beyond what a SMT solver can do, however you're not stuck with just using ATPs when they are supported. You can still allow for proofs to be manually written with an ATP doesn't work, and in fact SPARK allows for this with Rocq.

Most of what I have to prove is floating-point code where a manual proof is too much of a headache to ever attempt though.

> But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.

Sorry. See the edit at the top if you haven't already. I didn't realise how much it came off as a critique of you rather than a particular approach to software engineering.

It's easy to write something and have a model of what you're writing in your head that is massively different from how someone else will read it without realising, not that that excuses it.

---

I disagree with LLMs manually writing proofs without other tools doing all the work they possibly can ever being a good solution for a couple of reasons:

1. Tokens are really expensive when we have a LLM spending hours hacking aware at a proof, not to mention generating those tokens is slow.

2. The context window becomes flooded with proof work rather than work on the original problem, which will lead to a worse solution. LLMs are demonstrably worse at writing code when you continue a session on a new task instead of starting a new one.

> It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly.

We can cache the results and help the checker along with assertions rather than throwing out all the smart parts of the checker.

> "horribly broken or decades behind the current state of the art"

This is just about vibe-coded programs in general when the approach assumed by the article is taken. For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).

> I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax.

That's more or less what SPARK (and others) do, although specifications for large programs can become nasty.

I don't want to change that sentence now that people have discussed it, but I have added a note to the top to make it clear that I'm just taking it as an example of a vibe-coded program because it's recent and high profile.

My critiques of the language itself are not the main point, although I do still think that it's a very bad design to have a LLM waste tokens on a proof that could be written by CVC etc..

Yes, I didn't realise how much it comes off as a critique of the author personally when I wrote it. I have added a note to that effect to the top of the article.

> the author is clearly aware of formal verification, they've written several implementations of dependently typed languages

I'm not familiar with the author, I just saw the language posted the other day. I'll add a note to the top.

> These are different approaches with different trade offs.

Why would we want the tradeoff where the LLM has to write significantly more code and where the specification needs to be more complicated? If the author is aware of the state of the art then I think they made a poor choice, but that's not the point.

> Your post isn't clear, you don't go into any of these details

Bend just serves as a useful example, my general point is about how people will vibe-code a solution without an understanding of the field, leading to worse results than if they spent a little while understanding the field and then vibe-coded their thing.

MBD is a thing, however that doesn't really matter here, for making accessories you can more or less just assume all dimensions are perfect since you need some compliance for the accessory to be installable. What I'm talking about that can't be encoded in a model easily are things like the keepout area for the camera.

The reason you don't want Blender files at all in any sort of engineering is because it's a mesh. You can't pull any useful information, even something simple like a radius, from a mesh.