LiamPowell

> 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 they offer a service to make LLM-written text look human-written, if I recall correctly they even explicitly advertised that you could use it 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.

No decent engineering firm is going to want to work with FBX or Blender files. In fact they probably wouldn't even know what to do with them. Even proper model formats such as STEP files don't give you the details that are on a drawing that you actually need to do anything useful with these.

Why do you want you coding agents to be in a terminal? A terminal is missing latex rendering, inline images, a browser showing what the agent is clicking on, being able to view a spreadsheet and then select a region to reference in the conversation, clickable links when it references a specific line number with mouse-over previews, and interactive inline visualisations. A coding agent missing any of those is a significantly worse experience, yet people are for some reason willing to give up all of them to have their coding agents run in a terminal. It's not even like you get a familiar environment to work in, nothing that you set up in your terminal carries over into your agent or IDE.

I don't understand the trend of forcing everything into terminals. It's needlessly constraining and it's much more work that just using Qt (or any other UI framework).

It also incorrectly says that Emacs has no mouse support. When you first open Emacs the default buffer has clickable links in it, it's impossible to miss the fact that Emacs has mouse support if you ever even open it.

That's not what the comment you're replying to or the article says. I feel like I'm going crazy reading comments here and elsewhere, am I not reading the same articles as everyone else?

Note that all of the authors of this paper work for a company that sells this snake oil.

This entire idea of charging or discharging your body for some physiological effect is fundamentally flawed. It is indeed true that touching the ground will change your electrical potential to that of the ground, however that's as far as it goes, the rest is just nonsensical.

Let's start with the very first part of that, specifically changing your electrical potential to match the ground. The problem with this is that the ground is 0V because we define it as 0V, not because of any sort of fundamental property. Between two points on the Earth you can see hundreds of kilovolts. So the obvious question is why should the electrical potential of a particular piece of soil where your grounding rod is installed be physiologically preferable to whatever potential your body happened to be at before?

Now lets go on to the next part of what these scam artists usually claim. That is that the Earth's electrons enter your body and do good things of some description. When you touch the ground some small charge does enter or leave your body, however that stops nearly instantly when the potentials equalise[1]. How is the Earth meant to to keep putting electrons into your body if there's no voltage? That's just simply not how electricity works.

As an aside, note that I said enter or leave. A positive static charge and a negative static charge can both easily build up in your body. Therefore any claims that specify that electrons enter your body (or leave you body) is immediately nonsensical because it could go either way.

I'll leave it to someone else to explain all the nonsensical biological claims that follow on from the already fundamentally wrong electrical side since that's not my area. I will however note that none of these sponsored papers actually show and measurable biological effect, they all just hand-wave about redox reactions.

[1]: Yes, you're coupled to mains wiring and other changing fields that are around, however that's getting too far into the weeds for a short comment. If the claim made by the snake oil salesmen was that a current going through your body is good then they'd also suggest wrapping yourself in an electrical cord to maximise the effect, or just taping batteries to your skin.

Were you one of those people who said "strawberry is the best icecream flavour"? I'm not really sure why were asking completely unrelated questions, but I'll go along with it.

Though for the record, there was no community spread early in COVID where I am largely because there were approximately zero COVID deniers here: https://en.wikipedia.org/wiki/COVID-19_pandemic_in_Western_A...

I can't tell if this is really good satire or genuine. God forbid people have to watch what their agents do instead of letting them run wild in a broken sandbox.

Not just that, some actions spawn an entire Chromium instance. For example, any time you click on a music video (not a new thread, an actual full Chromium instance).

It's not even a build flag, it's a setting that you can just go and enable in Chrome's own settings menu (chrome://settings/content/v8).

It's useful to have all your tools automatically apply metadata in a standard way instead of having to keep track of it manually. Most cameras already add metadata that says what camera and lens were used, but you lose that as soon as you import it into Photoshop and export as a jpeg.

> However I question the value-add when e.g. the BBC website is already authenticated by nature of being served over HTTPS, and anyone who redistributes BBC content can and should link back to the source.

The value would be in images reposted to social media where the website an show a badge that says it came from a certain source.