8 ms·

Bend 2 and the Vibe-Coding Trap

• wg0 15d ago
  Some noteworthy lines from the README.md[0]: > - 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 https://github.com/bendlang/bend/tree/main
  • LightMachine 15d ago
    So are Haskell's, since 20 years ago, with no options for years? We will introducing binary buffers eventually. The project is new...
    • bunderbunder 15d ago
      “No options” simply isn’t true. Here’s a guide to many of the options: https://hasufell.github.io/posts/2024-05-07-ultimate-string-guide.html https://hasufell.github.io/posts/2024-05-07-ultimate-string-... 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.
      • LightMachine 15d ago
        Note that using linked lists for strings is actually more "parallel friendly" because you can take the head/tail and spread it around 16k GPU cores in O(1), unlike in Haskell, unlike arrays, which require a linear copy, becoming quadratic. So, the right "default type" isn't that clear on Bend, because GPUs behave very differently from CPUs. That said, yes, we definitely should have a compact Text type. I'll add it over the weekend.
        • bunderbunder 15d ago
          Though also, parallel processing strings and other non-numeric data on that level of granularity is, IME, typically less performant. The parallelism rarely manages to offset the performance penalties incurred by decomposing the problem in a parallel-friendly way. Even on a single machine you’ve got to think about whether organizing the data in a parallel-friendly way also makes it less cache-friendly. For example, a linked list of Unicode code points is 12 bytes per character, and each character might be on a completely different cache line. Depending on language a UTF8 buffer might be 1/10 the size and have a much more compact layout in memory.
          • ModernMech 15d ago
            Related: https://www.usenix.org/system/files/conference/hotos15/hotos15-paper-mcsherry.pdf https://www.usenix.org/system/files/conference/hotos15/hotos... We survey measurements of data-parallel systems recently reported in SOSP and OSDI, and find that many systems have either a surprisingly large COST, often hundreds of cores, or simply underperform one thread for all of their reported configurations.
            • bunderbunder 15d ago
              Yes, love that paper. Anecdotally I have a bit of a track record of 10xing slow systems’ throughout by converting them from distributed to single-node or from multithreaded to single threaded. Heck I once even sped up a number crunching operation by getting it off of the GPU and onto the vector coprocessor. Because GPUs also have a bunch of extra overhead to have to amortize away.
        • imtringued 14d ago
          Splitting a linked list is an O(n) operation. You can slice up arrays in O(1). The default type is incredibly clear to me.
    • mrkeen 15d ago
      To clarify, It looks like Haskell got better string types around 20 years ago.
  • jdiaz97 15d ago
    > > - The compiler (not kernel) is 99% AI-written and has not been fully audited yet. so vibecoded
• skybrian 15d ago
  It seems like this is largely a matter of what you’re asking for. If you wanted to do more research into the state of the field, an AI might be pretty good at answering your questions.
  • jchanimal 15d ago
    Yes, telling it that you want parsimonious solutions that reuse existing libraries makes a big difference. Why would it even try to do that sort of stuff if you didn’t ask?
    • deleted 15d ago
      [deleted]
    • Sharlin 15d ago
      Because it should be smart. I mean, why would a human coder ever observe standard best practices unless the client specifically asks them to?
  • vintermann 15d ago
    But it won't tell you if you don't ask. It won't tell you, "This approach is stupid, Ada SPARK exists".
    • Applejinx 15d ago
      Why would any LLM 'think' in terms of trying to cite prior work? 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.
      • skybrian 15d ago
        Nowadays AI chat often will do web searches and include links. It will do that more if you ask.
• pu_pe 15d ago
  The original discussion about the project (https://news.ycombinator.com/item?id=49746163 https://news.ycombinator.com/item?id=49746163) is very weird. Lots of call-outs about how the author is some sort of celebrity and random accounts vouching for him, with little discussion on the substance. Not even the demo on that release works well.
  • larodi 15d ago
    The whole original conversation was very smelly from the very start, 20k stars included on the GitHub page with lost history.
    • monster_truck 15d ago
      Does anyone know where they bought the popularity and contributors from? I would like to do this for my joke language to fool unsuspecting users into using it seriously
      • deleted 15d ago
        [deleted]
      • gf000 15d ago
        Probably at the same market where they sell snark. You may want to sell your excess of it, especially that as mentioned there were a popular (as in got to HN frontpage multiple times) version 1 and it's all legit and honest work, getting uncalled criticism?
        • monster_truck 15d ago
          Please do not shill your crypto here, nobody wants to buy snarkcoin
    • nylonstrung 15d ago
      Yeah 100% those are purchased/fake Lean4 itself has 9k
• IshKebab 15d ago
  Yes I think fundamentally the effort required to understand, write, and verify a formal specification is just way higher than is reasonable in most situations. 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.
  • rrook 15d ago
    Narrowly, I think you're spot on. The effort required to understand the machinery around formal verification is a function of the surface area of the thing being formally verified. Specifically, formally verifying the surface area of general purpose programming languages is difficult. 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.
• wg0 15d ago
  If you have to write LAWS.bend which is pure code describing the laws then it isn't basically like those old days of writing unit tests and that too tests first hence the TDD? 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?
  • hnhn34 15d ago
    > If you have to write LAWS.bend which is pure code describing the laws then it isn't basically like those old days of writing unit tests and that too tests first hence the TDD? There is a key difference: the laws are formally verified, as in Lean or Rocq (but much faster). So it's like writing a unit test or property-based test, but when it passes, you have a mathematical proof that you will get the expected output given ANY input in the infinite space of possible inputs. In traditional TDD, you make up some test case, write some asserts, and it passes if you get the expected outputs from those inputs and only those inputs. So you have to make multiple test cases for the same thing, and you still don't have any formal guarantee of your code's correctness. > Also, why the compiler is not written against and with LAWS.md so that no audit is required at all? Because it is mathematically impossible due to to Gödel’s second incompleteness theorem, which states: any consistent formal mathematical system strong enough to harbor basic arithmetic cannot prove its own consistency
• vintermann 15d ago
  "Know what to ask for" is what will keep me with a job for a while longer, I guess.
• GodelNumbering 15d ago
  The code itself is the most compact representation of the rules you want applied.
  • Smaug123 15d ago
    This is probably not necessarily true. “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone unless the program synthesiser is actively adversarial; probably 99.999% of the list-sorting in the world is done via standard library functions anyway, which suggests that people don’t much care exactly how it happens.
    • GodelNumbering 15d ago
      Good point. I would treat this as 'fully specified vs partially specified'. For a fully specified system, my mental model still maintains that the code is the most compact ruleset. 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).
    • someplaceguy 15d ago
      > “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone 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...
• simonw 15d ago
  > It will never tell you that what you’re building already mostly exists as work that you can build on. 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.
  • bryancoxwell 15d ago
    Think you could argue that’s more LLM-assisted engineering than it is vibe coding.
  • capitalatrisk 15d ago
    It seems implicit in the article that the author should have remembered to ask, as part of the prior research.
  • andrewjk 15d ago
    Isn't the usual argument that all AIs can do is build on prior art? Like, I spend a disproportionate amount of time trying to convince my agents that I don't want to just reimplement the Rust borrow checker for my language!
  • sigbottle 15d ago
    I really wish there were search harnesses, actually. My LLMs are lazy as hell and seem to want to just report the first thing they find on google. I know they can return truly niche and useful results, but it takes a lot more prompting to get them there than I would like.
    • eikonoklastess 15d ago
      you know that most big ai companies not only have search harnesses but also sota models that are post trained for web search specifically.this is what the deepsearch option is in most cases. and they have been unbelievably good for years now.
      • 15d ago
• mccoyb 15d ago
  @LiamPowell the author is clearly aware of formal verification, they've written several implementations of dependently typed languages, and ... despite the presentation of their work, which has some obvious flaws (as can be judged by reception) ... their many comments indicate that they know what they are talking about. 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?
  • LiamPowell 15d ago
    > 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.
    • Karrot_Kream 15d ago
      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.
• mentalgear 15d ago
  > The author of Bend has completely missed that this is the current standard in the field of formal verification, if they even know that this field exists at all. They have instead come up with this whole system requiring verbose specifications and even more verbose proofs. A little research before vibe-coding an entire language and compiler could have substantially improved the result because the author would have known what to ask for. > 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.
  • cmiles74 15d ago
    Or maybe it should be a flag to indicate that there might be more to think about before handing the task of to an LLM.
  • Forgeties79 15d ago
    > "run prior work research first". 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
• sligbad 15d ago
  Pro: it can be an excellent way to learn if you realize good problems don't come easy, many such cases where I abandon something having learned from it and that's life Con: the machine will tell you you have easily found a good problem, and engineered the perfect and necessary solution, if you let it
• deleted 15d ago
  [deleted]
• assumed_throwaw 15d ago
  I haven't seen a language launch this controversial on HN since V-lang in 2019. Glad we finally have some new drama to follow, definitely more entertaining than AI news.
  • deleted 15d ago
    [deleted]
  • serial_dev 15d ago
    It's definitely AI related, though.
• asfq-01 15d ago
  I think they know the standards of formal verification. They just surf the AI hype, whip up a verbose Python-like language that is worse than any existing prover language and have 20k bots star it. This is the way to succeed these days.
  • lemonlimesoda 15d ago
    [dead]
  • LightMachine 15d ago
    You just vaguely called the language "worse" without bringing a single concrete point. I can't defend my design choices without knowing what you don't like about it
• z7 15d ago
  > The field in question is formal verification. It’s notable that those two words appear nowhere on Bend’s webpage or in its codebase. The developer has built an entire language around a field seemingly without realising that said field exists. 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.
  • simonw 15d ago
    Back in 2018 they were working on Formality, an Ethereum formal verification project. They are the Victor in this video about it: https://slideslive.com/38911748/introducing-formality https://slideslive.com/38911748/introducing-formality Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs https://github.com/VictorTaelin/Formality https://github.com/VictorTaelin/Formality
    • LightMachine 15d ago
      Victor here. I haven't "worked" on Formality. I've founded it. Designed every part of it. Before LLMs! sighs Here's my response to this ridiculous accusation: https://news.ycombinator.com/item?id=49753898 https://news.ycombinator.com/item?id=49753898 I can't internet anymore. I need a beach
      • N_Lens 15d ago
        Sympathize with you mate, this article just seems like a poorly researched hit job.
        • verdverm 15d ago
          The article is about vibe coding, bend is the main character because it made frontpage. The author here says as much in the introduction, that it is not about whomever is behind bend, but the larger trend The author here has also added bend's author's link (in GP) to the original post, they very much do not seem to be doing a "hit job" and their intent is to comment on patterns from vibe coding
• deleted 15d ago
  [deleted]
• noodletheworld 15d ago
  I feel like this is the same black hole as small local models. 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.
• captainmuon 15d ago
  I haven't looked into Bend 2 in detail, but it seems a bit harsh to call it "horribly broken or decades behind the current state of the art". Clearly there is a problem with formal verification languages and there is a demand for something else in that area, and the problem is the usability and syntax. I don't want to have to learn something that looks like Haskell, or to have to wrap my head around Curry-Howard correspondence. I don't want to write my conditions in something that looks and feels like C++ template metaprogramming. I recall a Hello World in something like Coq a few years ago which basically started with "first, we construct the Peano integers", and then they used this to prove that some calculation was bounded - because it seems they couldn't represent integers natively? 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.
  • LiamPowell 15d ago
    > "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.
    • deleted 15d ago
      [deleted]
  • bunderbunder 15d ago
    It sounds like the crux of the issue here is that you don’t want formal verification in the first place. Your last paragraph sounds more like code contracts, which is also a thing that already exists.
    • captainmuon 15d ago
      Well, yeah, you have code contracts in Ada or Spec#, (very limited) fixed type ranges in Pascal, ... but no general purpose programming language lets you put an arbitrary expression in the same language in a type as a permanent condition, or lets you state facts that the compiler will prove. 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.
• mantovanidaniel 15d ago
  Finally a bit of sense in this madness.
  • rvz 15d ago
    The obvious botted stars on GitHub in 2 hours was an immediate red flag.
    • ospura 15d ago
      These stars are from version 1 of Bend
• vegnus 15d ago
  A language for LLMs will never be a compiled language. The best language for LLMs would be something that can be interacted with. Like a Lisp.
• auggierose 15d ago
  I wouldn't use SPARK either, and rather develop my own approach. The problem isn't that the proof has 400 lines of code, every modern system has large proofs (Isabelle/HOL, Lean, etc.) My latest formal proof has over 50K lines of proof. That's why AI is such a useful tool.
• mrbluecoat 15d ago
  > To be fair to Bend, I completely vibe-coded this, I just told a LLM to recreate the demo in SPARK A vibe-coded retort to a vibe-coding tool? Ugh.
• LightMachine 15d ago
  "The developer has built an entire language around a field seemingly without realising that said field exists." That is incredibly funny. Here's a talk about formal verification I made 7 years ago @ DevCon: https://www.youtube.com/watch?v=0fg1QbeeqNU 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 https://github.com/VictorTaelin/Cedille-Core I also implemented Kind-Lang 5 years ago, way before LLMs: https://github.com/higherorderco/kind 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.
• DannyBee 15d ago
  "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." 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.
  • svachalek 15d ago
    Good point, it's similar to music and other forms of art. The qualities that the people creating it care most about often have little to do with how well it is received.
• ycsucks2 15d ago
  [dead]
• hn45e7pbij 15d ago
  [dead]
• golol 15d ago
  I find this to be a mean and misguided post. To suggest that Victor Taelin does not know about formal methods. As I understand, he is trying to do something genuinely new and interesting. And he is transparent about his work, which he then gets hounded for. A shame.
  • dimgl 15d ago
    Why is it mean? The author is above critique?
    • suby 15d ago
      I found the post offputting because he is insinuating a few things about the author which are clearly untrue (eg, unfamiliar with the formal verification landscape) and he's using this untrue speculation as evidence of the dangers of vibe coding. Even the edit where he says swap it out with a hypothetical person who fits the description - it's still leaving in the untrue claims about the author. 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.
    • user43928 15d ago
      No, but the author seems to be above being critiqued for supposedly not even knowing of the existence of the field. Considering that he is a somewhat well known expert in the field who has been doing full time research on it for a decade.
      • suddenlybananas 15d ago
        https://scholar.google.com/citations?user=ZLnQcAsAAAAJ&hl=en https://scholar.google.com/citations?user=ZLnQcAsAAAAJ&hl=en This is not the google scholar of a well-known expert, I'm sorry.
        • vatsachak 15d ago
• orangelimetea 15d ago
  [dead]
• alxmths 15d ago
  > The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists. This is precious.
  • faize 15d ago
    The irony is that the author didn't even spend time to learn about the history of Bends author before writing this article.
• aviraldg 15d ago
  Very off-topic, but the 'humans write “laws”' phrasing made me think of using LLMs to unit test real laws. Have them come up with test cases to see if the phrasing is as intended or has loopholes. Wonder if anyone's tried doing something like this (probably not, I imagine this is too much tech for government)
  • slfnflctd 15d ago
    I guarantee you armies of lawyers have been doing exactly what you describe for years now with existing laws, and it's only increasing. 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.
• iswkq 15d ago
  This tells way more about you than Taelin. You didn't take a minute to research about Taelin, his past work, his company, and the design decisions behind the language. FFS, why people are like this.
• joshuaS98 15d ago
  If employer doesn't care about substantail 442 line fix, why should I?
• Jcampuzano2 15d ago
  This whole article can basically be summarized as "why is anybody building anything that already exists" gatekeeping. 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.
• davidw 15d ago
  As a resident of Bend, Oregon, checking the homepage sets off some kind of "oh look, Bend!" alarm in my brain.
• thomasahle 15d ago
  > Where this differs from Bend is that what we have supplied here is everything required to prove the correctness of the program, without having a LLM waste time and tokens on building up a 442 line proof from first principles. We can run GNATprove and get: `Success: all checks proved (12 checks).` 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.
• borzi 15d ago
  The vibe coding dunning krueger damage has yet to surface, but I'm guessing it will be in the billions. I'm not even talking about the insane infrastructure investments - thousands of c suite execs are vibe coding pointless crap instead of delegating it to their team that knows what they are doing, wasting thousands on tokens if they are on enterprise API plans for zero return or spending 30$ on creating an interactive html page for stuff that should be a power point slide with a few bullet points. It's totally insane!
• goldmoonx 15d ago
  [dead]
• goldmoonx 15d ago
  [dead]
• udomese 15d ago
  "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." 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.
• octoberfranklin 15d ago
  The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists. We need a catchy name for this phenomenon.
• johnfn 15d ago
  Pretty impressive to accuse the author of not knowing formal verification when even minutes of research would immediately prove the opposite (https://x.com/victortaelin/status/2100942399132312059?s=46 https://x.com/victortaelin/status/2100942399132312059?s=46, https://x.com/victortaelin/status/2100374221671051472?s=46 https://x.com/victortaelin/status/2100374221671051472?s=46).
  • deleted 15d ago
    [deleted]
  • ofjcihen 15d ago
    It’s unfortunate because what the OP describes is a real problem. Regardless of whether or not Bend2 is realistically usable or not, the author definitely does not fit the description of the type of people who are actually causing the issue.
• hmokiguess 15d ago
  > The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists. 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.
  • asgr 15d ago
    please, don't listen to Liam. The author is completely misrepresented in the blog-post :(
  • MasterScrat 15d ago
    I fully agree with this quote, it really crystallized something i felt but couldn’t put into words.
  • deleted 15d ago
    [deleted]
  • rozap 15d ago
    Agree with everything you say here. > 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.
• neuroticnews25 15d ago
  >Bend just serves as a useful example of my general point regarding vibe-coding as it is recent, high-profile, and has aspects that make it easy to use as an example. I don’t know anything about the author’s history with designing languages or if they actually did consider the tradeoffs below and made what I think is a poor choice 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.
• mohsen1 15d ago
  > A little research before vibe-coding an entire language and compiler could have substantially improved the result because the author would have known what to ask for. 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
• time0ut 15d ago
  I am a total outsider when it comes to this topic, but it reads like the author is doing the thing they are accusing the Bend 2 guy of. Good juicy reading while I sip my coffee!
• FoundAnotherOne 15d ago
  [dead]
• bluemoonx 15d ago
  [dead]
• madamelic 15d ago
  It absolutely drives me up the wall when I hear someone wrote their own language or framework because "the current ones just didn't do what I wanted to do" and then the result is a worse language/framework that the LLM and person know. 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?
• darksaints 15d ago
  I've been thinking about this a lot lately, because I've noticed a trend in my own life that has happened countless times: I have a tendency to look at problems that others in different fields have found difficult to solve, and think I have a great idea that could change that field. And then I push to develop my solution to that problem, run into real world problems with my solution, refine and adapt, try a different solution, run in a loop until I settle on the fact that the people who are in those fields also have great ideas, they just are more aware of the constraints and that's the reason why the hard problems don't have easy solutions. 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.
• turquoisemoonx 15d ago
  [dead]
• mromanuk 15d ago
  > The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists As a software developer we should fear chasing "better" solutions, that path always lead to procrastination, "kitchen sink" and probably not what users wants. "Good enough" should suffice in most cases. Sure if you are building a super mega critical software to land a plane or something like that, is different. But every day software, shouldn't be treated like "carved in stone" and stuff that should last a 1000 years. Code can be cheap now (calling it "vibe coding" doesn't help). You can create or modify something quite fast now. Better to focus on testing, documentation, making sure that software will do what is expected.
  • rafaelRiv 15d ago
    > As a software developer we should fear chasing "better" solutions, that path always lead to procrastination What a bad take. This is a discipline problem. You can chase both and be careful with the new solution.
• asgr 15d ago
  what a horrible blog-post :( Bend, HVM, Interaction Combinators, etc. isn't some vibe-coded fantasy, and the author has been working on this stuff for a loooong time. how incredibly disrespectful :/
• defgeneric 15d ago
  > Feel free to replace “the author” below with “a hypothetical author who could have created the same thing”. This is honestly sleazy, just admit you were basically way off.
• cwhy 15d ago
  All I see from this article and the whole saga is pure sadness. The situation seems unfortunate but seemingly unavoidable.
• Tehnix 15d ago
  What a weird reception there’s been to bend. People discrediting the author without bothering to look him up, and then getting defensive when others point out the fact that the creator of bend has a very long very public track record of work in the field. The irony of this post talking about vibe coding and not doing one’s research, on only not have done even the slightest inkling of research themselves (heck, even asking an LLM about the author would for sure have turned something up). I hope people will give it a second look, and not just stop at this post which is a gross misrepresentation of Victor Taelin’s work.
• gojongo 15d ago
  [dead]
• harrisonsmith32 12d ago
  [flagged]