Advertisement
Advertisement
⚡ Community Insights
Discussion Sentiment
58% Positive
Analyzed from 8986 words in the discussion.
Trending Topics
#author#don#llm#language#more#bend#vibe#research#llms#doing
Discussion Sentiment
Analyzed from 8986 words in the discussion.
Trending Topics
Discussion (189 Comments)Read Original on HackerNews
This example and Bend aside, I find this to be the biggest struggle with the perceived intelligence we have today. It's great at producing something that works, but it is not great at calling you out when you don't know what you don't know.
It's not able to educate and course correct you unless you have great self awareness and discipline.
That said, I think this goes for everything, it's easy to fall into this trap because it is very human. We simply don't know what we don't know, so it's not uncommon to revisit an old solution only to be enlightened that there is now new information that allows you to replace it with something much better.
I don't think anything here is new or changed, if anything changed is really just the rate that we experience this. LLMs make it easier and faster for the feedback cycle to happen.
Now back to Bend, I think putting your work out there and being unapologetic about it, open source even, and willing to take feedback, will go a long way.
I am more worried about the many closed source implementations of LLM built products that are being sold and people are depending upon that don't get this great criticism from many different thinking heads.
> I don't think anything here is new or changed
I would argue it's a little new though. I used to write dumb little programs all the time that explored an idea which was probably bad, and in that exploration I often found that there was a better way to do it, or that I didn't know as much as I thought I did, or that another thing already existed that was much better considered than my half baked idea, etc. But there was learning that happened there, so the process was still valuable. Now you can get a working bad idea without learning anything, there is full conservation of ignorance, but a full dopamine hit from "i made this thing". I guess you could argue it's just everything happening at a faster rate, but it feels different to me, and it is pretty eerie.
Before you would pause at overwhelming, now you get to "fail forward" with less at stake because the end result can still be verifiable even if the internals are a blackbox to you.
It's a sort of "deferred" and/or "optional" learning dilemma we now exist.
You could open the box, look inside, ask questions, but you would need to care and feel engaged, which is very hard to do when the result is already there.
This is why I framed it as requiring self awareness and discipline. Very easy to get caught into the slot machine dopamine cycle loop.
How can we "course correct" with "self-awareness and discipline"?
Not even the demo on that release works well.
I received several very emotionally charged responses centered in the personal credentials of the author. They felt very out of place and did not engage substantively with any of the things I said. It was indeed very weird
The author, who I hadn't heard of before yesterday, actually seems like a cool dude. He was quite responsive, normal, and engaged with my feedback, which makes other random accounts being offended on his behalf all the more uncanny
Your post and the ones that followed are a good example of the contrarian dynamic that dang often talks about. https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
In my own professional life, I've found this to be a very divisive statement. For some, it is a sign of wasting time and effort. For others, they use this to describe themselves when they want to do exploration for the goal of finding improvements, without any clear goal because they have a few ideas but none worth putting forward. I've been told to spend time learning AI and have found that saying "Yeah, I'm playing around with it." was the wrong thing to say because it was seen as not doing anything worthwhile. It doesn't matter that I would also say the majority of my tech skills were developed when I was "playing around".
I wonder if this is purely a linguistics breakdown, or if this is tied to some deeper difference in a person's relationship to tech?
I don’t see anything from your parent commenter on the other thread that deserves that classification. On the contrary, while they initially had suspicious of vibe coding, on later comments they are cordial and even admit their own misunderstanding.
What am I missing? Where does “called him suspicious as fuck” come from?
Edit: Answered below (https://news.ycombinator.com/item?id=49754311). Thank you.
If this is your first HN account and you haven't seen the site in the prior decade, the "emotionally charged responses centered in the personal credentials of the author" is the SOP. The site has yielded to that attitude because dang never enforced a sensible code of conduct, and relies mostly on favoritism and in-groups. Who says is more important than what is said, and the critiques you give are ranked according to whom you are critical of.
Think of this as a propaganda channel of a VC startup incubator who is brazenly looking for a product-market fit for anything and everything AI. Look at the roster of the recent startups and how many are AI-focused. Adjust expectations from there.
"I'm glad you're having fun vibecoding" comes across as very backhanded and condescending. It sounds like you may have actually meant that genuinely, but it doesn't read that way in text form.
"you sound sus af" is not respectful or constructive in my opinion. It's a description of your own feelings, not a critique of the project, and there's not really any way for the author to respond besides ignoring it or saying "sorry you feel that way" or something.
I think that line undermines the rest of your comment, because I'm left thinking that you don't really expect good answers to your questions and you just think the whole thing is dumb.
If I have years of experience on the topic and invested significant time into the project, I'd not be as civil as the author if someone came in and essentially called it vibecoded slop.
There is nothing weird about how others pointed out that the project appears to have merit contrary to how it at first might have looked to you.
[0] https://news.ycombinator.com/item?id=40390287
[1] https://www.youtube.com/watch?v=HCOQmKTFzYY
[2] https://www.youtube.com/watch?v=NaytZOiX3fs
> They just recycled the Bend1 repo for Bend2 even though it's a completely different language.
Why would you kill the source history of Bend1 completely if it has 20K stars? You can only do that if Bend1 has no users at all right?
Does that meant that Bend1 isn't actually successful in its own right but rather only as a marketing project?
I wasn't one of the suspicious people but I am now.
Lean4 itself has 9k
I can unequivocally claim that Victor receives at least two orders of magnitude more social media engagement, while Lean likely has 4-5 more magnitudes of actual users.
Serious users of Lean simply have no need or reason to star the repository.
Also, wrote a response to this whole thread here:
https://news.ycombinator.com/item?id=49753898
I would rather wait to see how it gets adopted, if at all. Anyone aware of early reviews of the adopters of bend 2?
Invariants were like "if outside temp < 40 or inside temp < 65: heater.minTemp( 65 )"
Axioms were like: "if {we're home} and it's {not a holiday} the house should be {comfortable temperature}".prompt
...and then that would get decomposed and translated into interlocking code for the scene(s). I'll have to look at this language a little more closely with those kinds of constraints in mind!
You're kindof translating `*.prompt` to either prolog (yucky!), lisp, lua, or javascript (for inspectability/debuggability), but this whole bend thing might be an exact fit for the problem space! Limited set of objects and states, bounded set of "invariants" (laws), and layering on top the general state modification activities (either "evaluated every 5 minutes and reconciled" or "set the scene xyz...").
By the time your first round of beta testing is over, you may have quite a handful of such axioms and variants, which have been humanly validated!
Have you done any such experiment in this space?
GNATprove uses SMT solvers, meaning it's basically a brute force proof system.
Yes, brute-force proofs are easier than symbolic proofs (lean, bend, etc.) because you don't have to supply a proof. It's all automatic.
But brute-force proofs don't scale to nearly anything of interest, which is why formal verification has been a niche field for 30 years, until now where LLM can write _actual_ proofs.
I checked the developer's X account, they have written numerous posts about formal verification, so this specific claim ("without realising that said field exists") seems to be false.
If the author of the article had done just a small amount of research about bend or it's author before writing the article they would have known pretty quickly what they were saying was incorrect.
I think the larger pattern here is that nuance is one of the most valuable commodities in the AI era. If you're hand waving stuff away without even missing , you're going to miss a lot of stuff in this cycle.
This article reminds me a lot of the famous hacker news Dropbox comment.
Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs https://github.com/VictorTaelin/Formality
sighs
Here's my response to this ridiculous accusation: https://news.ycombinator.com/item?id=49753898
I can't internet anymore. I need a beach
I am glad I saw it, as now I am interested in learning more about Bend.
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..
> Posts a link to real moon landing footage
I'd delete the article if I was you...
You know, in academia, they sometimes retract articles, even if they believe they are directionally correct
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).
I won't respond further.
Considering that he is a somewhat well known expert in the field who has been doing full time research on it for a decade.
It doesn't seem unreasonable to think it mean if I were to make up speculative negative assumptions about you which undermined something you've been working hard on for a long period of time.
I know nothing about the author, I'm just watching this whole spectacle unfold.
You are on the wrong side of this whole discussion, there is only one people here who needs calling out and it's not Bend's author.
Why is everybody treating this person like some celebrity. Am I weird for having never heard about this guy?
It would be weird to stand in line for throwing shit at someone you don't know anything about, and believing that the first guy throwing shit has an actual reason to do so.
It turns out everyone in that line is wrong..
I'm not a celebrity and I don't like celebrities
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. Dependent typing and design by contract for the masses.
Of course not, that would be equivalent to solving the halting problem, many people will say.
I wonder if that will change now: I'm happy with an imperfect sanitizer that I run every now and then and will run a couple of minutes and come back with: I've proved your conditions, I proved a violation, or I can't decide, please change your code.
Lean can be used as a regular programming language. There's also languages like idris2 and f-star, but they don't seem to have much traction.
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.
> This example matters beyond Bend, vibe-coding makes it makes it far too easy to implement a design that’s horribly broken or decades behind the current state of the art because you can immediately get a result without ever having to do any research. If you ask a LLM for a language where it’s possible to prove that a function is formally correct by building up a proof from basic principles then it will happily do so, it will never stop to suggest to you that computers can already build complex proofs without the need for a LLM and eliminate 99% of the work. It will never tell you that what you’re building already mostly exists as work that you can build on.
---
That's why all your LLM requests to build something substantial should start with "run prior work research first". Of course, at some point everything converges (if we share our outputs open-source) and then we may have solid standard patterns and libraries and do not need to waste trillions of tokens globally to rebuild the same minor, fundamental things, each one in their silent little silo.
IF we share, it will be of course to the monetary detriment of LLM providers who will have less income overall, and of course now they can't repackage anymore all our collective input, thoughts, human 'thinking traces' that they collect in their meta-data, as their new 'innovations' any more to inflate IPOs / stock prices.
The searches it runs, and the summaries it provides, are all incredibly sensitive to your choice of words. Words you chose from a state of minimal knowledge. So it’s like a particularly perverse version of the anchoring bias: information that could have led you to a better solution is often actively filtered out of the agent’s response precisely because it leads down a different path from your first idea.
In short, if you ask an agent what’s the best hammer for driving screws, it’s liable not to mention that screwdrivers exist.
As in, are you sure, and can you provide concrete examples?
And yes the output of these researchers are highly sensitive to prompting. Left to their own devices the LLM will often ship some very biased prompts to its deep research agents loaded with pre-conceived ideas rather than letting the agents uncover things themselves. Then all the agents do is confirm what the prompt told them to rather then “think independently”. (Very similar to open ended interview questions rather than asking yes/no questions)
It’s is far better to spend a session writing writing the research prompt itself.
All of this takes time and tokens of course…
Yes, but I think there are incentives to not do this for many LLM providers. Doing prior-work research is slow (web searches aren't fast, LLMs are rate-limited or blocked from plenty of pages, etc.), and sometimes contradictory which annoys LLM users, many of whom like faster gratification cycles from the agent slot machine handle.
Also, writing a bunch of bespoke code instead of leveraging prior art makes a lot of users feel like they own something novel/big/important, and also poses a larger maintenance surface for the LLM to make future changes (which costs tokens).
I don't think there's, like, a conspiracy at LLM providers to set up system prompts/RAG/etc. to discourage research-and-use-prior-art-by-default approaches. Rather, OpenAI/Anthropic/Google/etc. are optimizing for real but sometimes misleading success metrics which often lead away from a research-first approach.
- But that shouldn't be confused with getting the LLMs to make the decisions. I believe that would quickly ruin a good design, unless the decisions are about truly inconsequential aspects, which are very rare in language and API design.
- I don't believe that (sharing) is to the detriment of LLM providers either. Not realistically. We would build faster and the questions / research directed at LLMs would be more sophisticated. Believe it or not, they can't cache questions as easily as websearch queries. If anything, I believe the more people learn to use LLMs effectively (rather than just to generate slop), the more their usage will be ingrained in daily life. Some of that will be redirected towards current LLM providers. But perhaps more of the economic share will increasingly go to hardware providers, as more and more people will be interested to run their own models.
As effective as “make no mistakes.”
It is trying to please you, and it always determines that the way to please you is to fulfill the original, core request. Any caveats or first steps will always be secondary to the ultimate goal of “this person wants to do X, so I will do X.”
The only first step I have found somewhat consistently useful, because as we know LLMs do not behave consistently, is when doing tech troubleshooting I will go “look at documentation for X before answering” so that it will search manuals and such. Helps avoid speculation. But even then, it’s still not full proof.
Sidebar: this is one of the core problems of LLM’s currently. You are basically arguing with them to get them to behave a certain way all the time and it’s not always clear if they’re doing what they’re being told to do. Then add the compounding layer that the longer the conversation goes on, the more likely it is to misunderstand or just ignore things as it descends into context-length-induced madness
Those aren't comparable instructions. Providing useful, related context to improve outcomes is a basic best practice, and asking LLMs to do research first is an important source of that.
A little research before writing and publishing a personal attack like this could have substantially improved the result because the author would have known what they're writing about
Victor is not a formal verification noob as this article suggests
> - The compiler (not kernel) is 99% AI-written and has not been fully audited yet.
> - Strings are linked lists of characters, so text processing is slow.
[0]. https://github.com/bendlang/bend/tree/main
so vibecoded
We will introducing binary buffers eventually. The project is new...
Now if you’re asking why the basic prelude String type remains as it is, that’s because changing it would break more code than it’s worth, at least as far as prelude’s maintainers are concerned. This is no different from how standard C strings remain a null-terminated sequence of bytes even though that’s been awful for everyday use for at least 30 years.
That said, yes, we definitely should have a compact Text type. I'll add it over the weekend.
There is an absolutely enormous amount of hubris to being an engineer. I don't necessarily think its a bad thing...a certain amount of hubris is necessary for progress to be made. Our minds are creative and we can come up with amazing things, but something in there always makes us think we can do it better than the people who are stuck doing it daily. We fool ourselves into thinking they're too stuck in their mindset to have a more creative solution.
And the funny thing about LLMs is that while they can enable our competence, they enable our hubris even more.
So what is the unique idea here except a vibe coded compiler that generates C and everything else is handled by clang+llvm?
From README.md:
>The compiler (not kernel) is 99% AI-written and has not been fully audited yet.
Also, why the compiler is not written against and with LAWS.md so that no audit is required at all?
It will if you remember to ask it. I've got into the habit of starting any new project with a session where I ask a search-enabled LLM to help me figure out what the prior art for a problem is. It's saved me quite a bit of time.
See also this piece on misalignment from OpenAI https://alignment.openai.com/misalignment-reports/self-gener... which reveals one of their RL tasks:
> In mid-2024, <redacted> published a list of the best books of the 21st century selected by a panel of experts. It also published a separate list based on readers' votes. I would like to know whether my local public library's collection included the books on the latter list as of August 24, 2024. Consider only the top 50 books, and exclude nonfiction and poetry collections.
It would also make sense for them to just RL in the "research prior art" arc as part of that "is the request sensible" pre-analysis. It wouldn't be difficult and it would save everyone a lot of pain.
Glad we finally have some new drama to follow, definitely more entertaining than AI news.
That is incredibly funny.
Here's a talk about formal verification I made 7 years ago @ DevCon:
https://www.youtube.com/watch?v=0fg1QbeeqNU
Here's Cedille Core, my implementation of Aaron Stump's self types, a Computer Science professor who taught me a lot, ~8 years ago:
https://github.com/VictorTaelin/Cedille-Core
I also implemented Kind-Lang 5 years ago, way before LLMs:
https://github.com/higherorderco/kind
I dropped out of Federal University of Rio de Janeiro to study this subject independently, because I was passionate about it, and I spent nearly 10 years doing so, daily, on weekends. That's what I do.
Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists. Kind had these, 5 years ago. In fact, I've also been researching the later, and I built SupGen, which overperforms every published symbolic program synthesizer in the literature by 10x or so. This is unpublished yet, but you can find my posts about it 2 years ago on X (I'm @VictorTaelin).
So, why is Bend verbose???
Because it makes it fast. It is intentional. It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly. That is what makes Bend realistically 10x-100x faster than every alternative.
But wouldn't that mean it is much harder to write it?
No. As you said it yourself, we have tools that can fill these proofs today! Not just AI models. You can apply these tools to produce Bend proofs, while the language itself remains a thin, dumb proof kernel that does one thing, and does it well.
If nobody is reading these proofs (because they're written by AI and automated tools), then, it is, in my opinion, irrelevant, as proofs will eventually become a layer nobody looks at, just like generated assembly.
Of course, I could be wrong here!
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.
Every single part of Bend is an intentional choice I made after considering every alternative. I use LLMs to fill code after I make all hard architectural decisions because they type faster than me, and I'd rather spend my time doing useful experiments than typing trivial functions, even though I could.
Incidentally, deciding what I should NOT include took me way more time and effort than any line that was shipped, and there are perhaps millions of lines of code, manually written by me, that I threw away, backing up these 4k that went into the final design. An artist once told me you must first paint a Rembrandt before you can draw a cartoon that's simple in the right way, yet that might mislead someone who has never drawn into thinking you don't know what you're doing. I guess.
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.
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.
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.
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
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.
Clearly the author knows what he is doing, even if you think it isn’t a sensible approach.
It might still be true that LLMs make it too easy to create a broken design and don’t warn you if you ask for something already exists.
The thing is, the example you decided to pick on does not work.
You accused the author of having fallen into the ‘vibe-coding trap’. He clearly did not.
Sorry about what? Getting caught? You entire post is based on a nasty lie about Victor and his work.
I'm just leaving you a comment to counter the influx of negativity coming towards you for no reason.
I hope you are doing well and won't take all this too badly -- try to think of it as just free marketing for your project!
Have a nice day!
> I use LLMs to fill code after I make all hard architectural decisions because they type faster than me, and I'd rather spend my time doing useful experiments than typing trivial functions, even though I could.
Are you being facetious? Because I've seen some bad takes from people trying to justify their AI coding practices, but this is the first one that actually made me laugh. It's clear that this public attack has you in a defensive mental state (which is perfectly understandable), so giving you the benefit of the doubt, I won't pile on and take everything you're posting too seriously.
However, I gotta point out how ridiculous this statement is, because it's the kind of thing that'd make me wonder if someone has any programming experience at all. Typing speed is not, never has been, and never will be a limiting factor in software development. "I didn't do <X> because of <reason> even though I totally could" is a pathetic cope.
It kinda reminds me of a recent post from John Carmack where he said (paraphrasing) that he originally wanted to release Idtech to the public domain as a "gift to the world", but couldn't do it because of his pesky business partners, but he totally would've done it. Let's just ignore the part of the story where he became filthy rich from licensing his software, and focus on how good it will feel to call it a "gift to the world" when an AI company integrates your code into their commercial products without licensing it from you.
Do you have benchmarks which show this?
A vibe-coded retort to a vibe-coding tool? Ugh.
For new legislation, you may have a point in certain situations, but even the most clueless Congress critter has people working for them who get this stuff. Whether they choose to consult them or not is, of course, another matter entirely.
This is the way to succeed these days.
I absolutely endorse new creations when they are necessary but the people making these aren't doing it from a point of education, they are doing it purely because _they_ don't understand the framework or language that is the standard for that area.
It always always always involves a high level of AI Psychosis, that a brand new web framework is needed for your revolutionary... CRUD app?
I agree that "don't care" is often the practical choice which corresponds to partially specified. In your sort example, both heap sort and merge sort satisfy the requirement. But they are not always interchangeable because each has a specific properties that you might care about (constant memory vs nLog(n) memory, easily parallelizable vs hard to parallelize and so on).
Not good enough: `f(x) = []` or `f(x) = (if len(x) == 0 then [] else [x[0], x[0]]` are implementations that fulfill your specification and yet they don't always sort the input list correctly...
Your post is setting up a strawman between automatic formal verification and formal verification using interactive theorem provers ... obviously there is a spectrum, and Ada/SPARK are navigating the space to try and automate much of the work required to automatically dispatch with obligations to prove (computable) properties about programs.
Bend2 is a QTT -- it's dependently typed, and comes from the lineage of systems which are focused on being expressive enough to formalize mathematics.
Of course you need to build a somewhat significant "standard library" of theorems, tactics (as metaprograms), etc ... to approach what is built into the compiler in Ada. These are different approaches with different trade offs.
Your post isn't clear, you don't go into any of these details ... why did you post this? Do you think this is clear writing?
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.
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)
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.
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.
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.
> 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...
I don't know what llm you use but current llms will definitely let you know about similar things out there. So this statement is a bit incorrect.
This doesn't make any sense, you're equivocating vibecoded as in "prompted by a clueless incompetent person" with vibecoded as in "implemented by an LLM". Former is used to make your point, later is used to defend the premise.
It itself is prior work. It's asking a fish to show where the water is. The fish can't imagine that absence, and the LLM can't imagine anything not being prior work.
Con: the machine will tell you you have easily found a good problem, and engineered the perfect and necessary solution, if you let it
Despite the fact that the entire premise is incorrect since the author of the language clearly has been shown to know about formal verification, this is basically encouraging nobody to ever post anything they work on for fear it might be "similar" to something already out there.
Is this really where we want the industry to go to all because of vibe coding?
The author of the article itself also clearly did 0 research of their own at all on the author of the language, and admits to vibe coding their own example themselves.
What the fuck are we doing.
This is precious.
This is totally true but almost totally irrelevant. I'll use some hyperbole here to make the point: Whether the design is broken or decades behind doesn't matter anymore. Neither of those are an outcome/end goal. They are means we historically have used to achieve good end goals or outcomes.
In the end, the goal is usually "does it meet the needs of the person who needed it" not "is it good software". If it no longer meets their needs and they can vibe code another total piece of shit in an hour that meets their needs again, they still may be "better off" than spending time researching the field and learning and ...
This may feel shitty, and it may feel like it should not be true. But right now, that seems to be true?
In that sense, the author is wrong that vibe-coding is a trap. The trap is assuming you have to make something good to meet someone's needs both now, and in the future.
Now, like i said, this is hyperbole, and there are lots of good arguments against it. The author's just isn't one.
Technically good or better has never mattered very much in the marketplace, despite people wanting it to really badly (ease of use often mattered, but not technical goodness). Software engineers often took pride in their work and so there were usually kernels of goodness in even the shittiest software. All you are seeing is that now it is nowhere near as hard to create and bring these "solutions" to market, and more importantly, doesn't necessarily require anyone who has any pride in their work at all, or even have any experience in software engineering. As such, technical goodness has mostly gone out the window because the market never required or really rewarded it.
We need a catchy name for this phenomenon.
There are some cases where it is pleasingly simple - usually low level algorithms like compression, sorting, search etc. Basically things you'd find in leetcode questions.
Most software isn't like that.
I think the actual answer is just that the very latest models (e.g. Astra) are actually quite good at writing normal tests, and you can just skim them to make sure they're doing something sane.
My approach with Hale (shameless self plug) is that the programming language itself first offers another strata of structure to program within, a type of graph. Once the structure of the program is expressed as a graph, understanding how formal verification works is a clean encapsulation of graph activities.
Things people want to be awesome and true, and things that are actually awesome and true don't intersect the way people want them to.
…so if there was an easy way to do provably correct AI code, it would be nice.
…but I’d also like a frontier that runs on my raspberry pi and a cheap fully autonomous self driving car that just uses a single cell phone camera.
Unfortunately wanting those doesn't make them exist; and people telling you they do exist usually are either a) uninformed, or b) selling something.