> 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.
I would encourage you to think more deeply about the assertions you're making here.
I've done a fair amount of work in this space as well, specifically my main toolbox of formal verification tools in the past have been Rocq, Idris, Dafny, and TLA+, and I can say that I've come away with roughly the same set of tradeoffs as what LightMachine describes in his comment.
Current formal verification tools are often very slow precisely because they try to reduce the number of lines of code that are required to write a proof. By making proofs more verbose and more explicit, proofchecking is sped up immensely (my own experiments check out with what LightMachine is saying here; indeed I've seen even greater speedups in the range of 100-1000x).
It makes far more sense to pay a series of one-time costs in LLM tokens that reduces your compilation time from 1 hour to 1 second than to pay the 1 hour compilation cost again and again (these are not exaggerated numbers for larger projects). This is especially true because with modern LLMs, it's usually just fire and forget and let it churn in the background than anything else.
Caching and incremental compilation has a lot of limitations, e.g. for CI. This is the promise that languages like GHC Haskell have promised for a while that always gets blown away by the other side like OCaml where global compilation is just so fast that you don't have to deal with those limitations.
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.
> You don't have to let the ATP do everything, you can speed it up immensely with well placed assertions where it struggles.
This is basically what you do with Dafny. I'm not very happy with this, not least of which is because it makes for an inferior developer experience in my opinion and because in general you are pretty limited in expressiveness of propositions.
Also it's kind of weird to be fixated on ATPs, as those are more or less a different level of abstraction from the language. You could develop an ATP for Bend.
More generally speaking, the largest, most well-known formal verification projects that verify actual code don't really rely on ATPs. SeL4 relies on explicit proof terms, CompCert relies on explicit proof terms, etc.
Silly question, but in Rocq, just for example, what does prevent you to fire `auto`, then, when it solves the goal, to just substitute it in your proof with the term that it constructed? Not calling you on BS, but genuinely interested in the problem
This significantly helps compile times, but will still end up with something far slower than Bend. What was I was talking about and presumably what LightMachine is talking about is how Bend is significantly more verbose than Rocq because even if you wrote out everything with terms, Rocq is still substantially slower than Bend, because Rocq relies a lot on implicit machinery (much more significant elaboration, implicit args, etc.) that slow down compilation.
Just don't use frontier models by American labs. Chinese models are much cheaper and competent enough for most stuff
> 2. The context window becomes flooded with proof work rather than work on the original problem,
This can be solved by doing proofs in subagents. You can even have a tree of agents, for demanding proofs. They can share a database or otherwise have communication channels if some of them stumble upon something relevant for another agent
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.
Nowadays agents know a lot of tricks on how to effectively prompt subagents
Generally speaking the ouput of a subagent is sent directly to the calling agent, that can make the final edits. Or, the subagent can edit the file in a local copy, and the calling agent can diff it
1. LLM inference is cheap compared to the cost of a bug, and you can use tools to automate the proof-work, as you said so yourself.
2. Why would it? The AI shouldn't load already completed proofs, only their type signatures (which are one liners). Sounds like you're projecting bad context management?
Caching only works until you change a deeply nested constant. Then you must wait 2 hours as Lean re-checks every transitive dependency of a massive simp-ridden codebase. Also, first time check time IS relevant to UI. Nobody wants to wait 2h to start using a library after they first download it. Perhaps you don't mind that but I do; that's the kind of bad UX that made me go for that design choice on Bend. Which again, may be wrong or may be right. But it was intentional.
Having a checker that is just fast by construction, regardless of caching, was a top design priority, and I weighted it over verbosity in a layer I believe nobody will be reading anyway.
> 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.
I'm curious, have you actually tried Bend (for more than 5 minutes)? Or are you more of an expert on this topic than the author who has been deeply immersed in this for 10 years, after it's single day of release? From an outsiders perspective it feels like this is personal to you, and you're being unfairly critical.
It will, there is just too much to do! It is a programming language. With a consistent, non-standard proof system. That compiles to GPUs. We're a small team. Please be patient
Because it's a toy problem and I would definitely not take much away from it. Most proofs are basically write-only and impossible to maintain -- you are better off throwing it away. And I mean human-written formal verification here, like Coq and Agda. Take a look at formalized mathematics, they are absolutely massive code bases.
I think people don't have an intuition of LLM costs and the time saved by using it. Of course it costs but its obvious that it brings more in savings than it costs.
Post author just wanted quick clicks based on kneejerk heuristics based attacks on Bend. Now he’s doing gymnastics all over this thread to mitigate what he said. Sad and disappointing.
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).
Your only issue was that the author was unaware of a subject and that the code is long. You didn’t even google the guy! Respectfully, I think you made a bad point and probably harmed your own stance with this post.
Expensive compared to what? Vs. human writing proofs they're definitely not.
> The context window becomes flooded with proof work
Context management is more art than science, but proofs are unusually good at compactation. Once proved, you can just keep the lemmas, you know,like humans do.
> "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..
you know what's the least you could actually have done instead? no, you don't need to retract the blog post at all, keeping it up was the right choice.
Now slap a big ass apology for being an unaware snob on top of it instead of leaving a link to the author's reply, like an after thought.
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.
But this is grossly intellectually dishonest. You know very well how this will be read and responded to here ... and you keep saying that you're just talking about vibe-coding oh but you have serious criticisms of the specific effort. You write passive-aggressive stuff like
> For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).
which contradicts your base assertion that their decisions were not informed. And
> My critiques of the language itself are not the main point, although I do still think that it's a very bad design ...
You claim
> The developer has built an entire language around a field seemingly without realising that said field exists.
but that is severely factually wrong, which along with a lot else suggests that you have very bad judgment. As the author writes,
> Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists.
IOW, you have made a serious error in logic.
> To be fair to Bend, I completely vibe-coded this
Some advice: DBAD
You trashed the author and his work without bothering to learn anything about either one first (which is quite ironic).
> 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.
Perhaps because their concerns are different? Similar reasoning: "why invest in dependently typed languages over SMT solvers? SMT solvers are automatic, and it is way easier to add annotations to my programs"
The answer is that these technologies are not universal in trade off space.
Of course, if you can have an LLM prove something by dispatch to an SMT solver ... you want to do that (and, indeed, LLMs do sometimes do this even when working on Lean proofs)
But the space of statements that you can prove using verification with SMT is smaller than dependently typed systems.
Also, Ada/SPARK are very good and robust -- they've been around for ~50 years ... but there's been a significant amount of work in formal verification since then, right? I would be more clear that Ada/SPARK are state-of-the-art for "mission critical software" (and have been for many years), but there's been a lot of research work in formal verification of low level programming since then (Low*, for instance)
I'm assuming you have not spent a lot of time trying to prove stuff about non trivial programs if the trade offs between SMT based approaches and interactive theorem provers are not clear to you.
SMT solvers are highly automated, but very opaque and hard to debug. Interactive theorem provers can scale to larger problems and harder properties at the cost of increased manual proof burden. The ever increasing ability of llms to write proofs in a theorem prover has in recent years tipped the balance significantly towards preferring itp based approaches over pure SMT ones. The current state of the art for program verification is probably a mix of llm and traditional (tactics, SMT, etc.) proof automation inside an itp.
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.
If you're going to insinuate that the author of Bend2 doesn't understand PLs and formal verification, you should do so with some proof and not a hot take dunk.
I think it's fine to critique the language and the approach without criticizing the author and I hate that this site has become Tech Drama News, like the worst parts of Twitter.
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.
conversations on this site about formal methods are currently absolute cess pits of dunning kruger and confidently stated yet highly misinformed takes from those with close to little experience in the field.
I think sadly all big conversations on this site are like this these days. It didn't used to be like that sadly. Z3 and some early Lean threads used to be great.
You clearly don't know shit about the whole topic, yet attack an open-source project's author who wasn't even the one posting his own project..
> 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.
Because code is trivially cheap now. LLMs churn out a shitton of code at pennies, and as technology improves their per-line cost will continue to decrease. A proof has to be written once and it's never read again. It's only important property is that it is machine-verifiable - from then on only the signature matters. Meanwhile speed of compilation matters, so an obvious tradeoff was made by the author.
> 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.
This is clearly not the case here, and even if it were, it's still a better thing than vibe-blogging clickbait shit with extra amount of Dunning–Kruger. Calling out an author who clearly works in the field for a decade or more for not knowing the topic...
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.
I’ve only dabbled with cad for 3d modelling in Onshape. It seems that there all kinds of ways to add measurements in the render files. Not sure about blender.
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.
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).
For me it’s that why do I need another application open? I have my coding agents in the terminal, I should also be able to traverse and read a codebase in the terminal as well
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.
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?
There's a lot of unverified hearsay but the crux of the problem is that there is controversy around using this company's tools, the attribution of the resulting work, and the company for some reason competing with its users. The whole thing reeks and my point is: people won't ask for the chromatography spectrum of the turd, they will walk away.
reply