HN

Comments (137)

• thomasahle
  > 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.
• Menu

  pu_pe
  The original discussion about the project (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.
• Menu

  z7
  > 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.
• Menu

  captainmuon
  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.
• Menu

  golol
  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.
• Menu

  mentalgear
  > 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.
• borzi
  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!
• Menu

  wg0
  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
• wg0
  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?
• udomese
  "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.
• Menu

  assumed_throwaw
  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.
• Menu

  simonw
  > 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.
• Menu

  LightMachine
  "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=0fg1QbeeqNUHere'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-CoreI also implemented Kind-Lang 5 years ago, way before LLMs:https://github.com/higherorderco/kindI 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.
• mrbluecoat
  > To be fair to Bend, I completely vibe-coded this, I just told a LLM to recreate the demo in SPARKA vibe-coded retort to a vibe-coding tool? Ugh.
• Menu

  aviraldg
  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)
• Menu

  GodelNumbering
  The code itself is the most compact representation of the rules you want applied.
• octoberfranklin
  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.
• anon
  undefined
• Menu

  mccoyb
  @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?
• auggierose
  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.
• Menu

  skybrian
  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.
• joshuaS98
  If employer doesn't care about substantail 442 line fix, why should I?
• Jcampuzano2
  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.
• sligbad
  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 lifeCon: the machine will tell you you have easily found a good problem, and engineered the perfect and necessary solution, if you let it
• Menu

  asfq-01
  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.
• vintermann
  "Know what to ask for" is what will keep me with a job for a while longer, I guess.
• vegnus
  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.
• Menu

  alxmths
  > 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.
• davidw
  As a resident of Bend, Oregon, checking the homepage sets off some kind of "oh look, Bend!" alarm in my brain.
• anon
  undefined
• Menu

  IshKebab
  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.
• DannyBee
  "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.
• noodletheworld
  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.
• Menu

  mantovanidaniel
  Finally a bit of sense in this madness.
• hn45e7pbij
  [dead]
• orangelimetea
  [dead]
• ycsucks2
  [dead]
• iswkq
  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.