Hacker News Reader

I was really confused when reading the article that their claim is you don't know formal verification, I was expecting something way juicer.

> But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.

Sorry. See the edit at the top if you haven't already. I didn't realise how much it came off as a critique of you rather than a particular approach to software engineering.

It's easy to write something and have a model of what you're writing in your head that is massively different from how someone else will read it without realising, not that that excuses it.

---

I disagree with LLMs manually writing proofs without other tools doing all the work they possibly can ever being a good solution for a couple of reasons:

1. Tokens are really expensive when we have a LLM spending hours hacking aware at a proof, not to mention generating those tokens is slow.

2. The context window becomes flooded with proof work rather than work on the original problem, which will lead to a worse solution. LLMs are demonstrably worse at writing code when you continue a session on a new task instead of starting a new one.

> It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly.

We can cache the results and help the checker along with assertions rather than throwing out all the smart parts of the checker.

1. LLM inference is cheap compared to the cost of a bug, and you can use tools to automate the proof-work, as you said so yourself.

2. Why would it? The AI shouldn't load already completed proofs, only their type signatures (which are one liners). Sounds like you're projecting bad context management?

Caching only works until you change a deeply nested constant. Then you must wait 2 hours as Lean re-checks every transitive dependency of a massive simp-ridden codebase. Also, first time check time IS relevant to UI. Nobody wants to wait 2h to start using a library after they first download it. Perhaps you don't mind that but I do; that's the kind of bad UX that made me go for that design choice on Bend. Which again, may be wrong or may be right. But it was intentional.

Having a checker that is just fast by construction, regardless of caching, was a top design priority, and I weighted it over verbosity in a layer I believe nobody will be reading anyway.

I think people don't have an intuition of LLM costs and the time saved by using it. Of course it costs but its obvious that it brings more in savings than it costs.

> you can use tools to automate the proof-work, as you said so yourself.

The language doesn't appear to be designed around supporting existing tools (either by exporting to Why3 or manually interfacing with existing tools). I'm not against shipping the whole proof or storing it on a cache server, I'm against the idea of having a LLM write it all. Even having the LLM only write proofs for subprograms that take a long time for ATPs to prove would work.

For the example in the article, the LLM had to write it exactly once without any iteration and it proved in a second, which I assume was mostly startup time. Having a LLM write 442 lines instead, which I assume also needed some iteration, is a tough sell in comparison.

I'm curious, have you actually tried Bend (for more than 5 minutes)? Or are you more of an expert on this topic than the author who has been deeply immersed in this for 10 years, after it's single day of release? From an outsiders perspective it feels like this is personal to you, and you're being unfairly critical.

It will, there is just too much to do! It is a programming language. With a consistent, non-standard proof system. That compiles to GPUs. We're a small team. Please be patient

You mean the SPARK example?

Because it's a toy problem and I would definitely not take much away from it. Most proofs are basically write-only and impossible to maintain -- you are better off throwing it away. And I mean human-written formal verification here, like Coq and Agda. Take a look at formalized mathematics, they are absolutely massive code bases.

> Tokens are really expensive when we have a LLM

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.

> 1. Tokens are really expensive

Just don't use frontier models by American labs. Chinese models are much cheaper and competent enough for most stuff

> 2. The context window becomes flooded with proof work rather than work on the original problem,

This can be solved by doing proofs in subagents. You can even have a tree of agents, for demanding proofs. They can share a database or otherwise have communication channels if some of them stumble upon something relevant for another agent

The problem with using subagents is that you often have to rewrite a chunk of a program in a more proof-friendly way, just saying "go prove this code, don't edit it" doesn't work. Maybe I'm underestimating how effectively subagents can communicate though and they'd be fine asking for changes.

Nowadays agents know a lot of tricks on how to effectively prompt subagents

Generally speaking the ouput of a subagent is sent directly to the calling agent, that can make the final edits. Or, the subagent can edit the file in a local copy, and the calling agent can diff it

Moving the goalposts a bit here, aren’t you?

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.

Post author just wanted quick clicks based on kneejerk heuristics based attacks on Bend. Now he’s doing gymnastics all over this thread to mitigate what he said. Sad and disappointing.

Yes, I used Bend as an example because it is recent and high profile, and I also wanted to present my issues with it. I did not mean to conflate it with the main idea I was trying to present to the degree that I obviously did after reading my own writing as a third party would (at least to the degree that it is possible to do so).

Your only issue was that the author was unaware of a subject and that the code is long. You didn’t even google the guy! Respectfully, I think you made a bad point and probably harmed your own stance with this post.

>Sorry. See the edit at the top if you haven't already.

Sorry about what? Getting caught? You entire post is based on a nasty lie about Victor and his work.

I would encourage you to think more deeply about the assertions you're making here.

I've done a fair amount of work in this space as well, specifically my main toolbox of formal verification tools in the past have been Rocq, Idris, Dafny, and TLA+, and I can say that I've come away with roughly the same set of tradeoffs as what LightMachine describes in his comment.

Current formal verification tools are often very slow precisely because they try to reduce the number of lines of code that are required to write a proof. By making proofs more verbose and more explicit, proofchecking is sped up immensely (my own experiments check out with what LightMachine is saying here; indeed I've seen even greater speedups in the range of 100-1000x).

It makes far more sense to pay a series of one-time costs in LLM tokens that reduces your compilation time from 1 hour to 1 second than to pay the 1 hour compilation cost again and again (these are not exaggerated numbers for larger projects). This is especially true because with modern LLMs, it's usually just fire and forget and let it churn in the background than anything else.

Caching and incremental compilation has a lot of limitations, e.g. for CI. This is the promise that languages like GHC Haskell have promised for a while that always gets blown away by the other side like OCaml where global compilation is just so fast that you don't have to deal with those limitations.

You don't have to let the ATP do everything, you can speed it up immensely with well placed assertions where it struggles. Maybe a hybrid approach is best where we run ATPs with a very low timeout to get all the easy stuff and then have a LLM write a proof using the thereoms that the ATPs were able to prove.

> You don't have to let the ATP do everything, you can speed it up immensely with well placed assertions where it struggles.

This is basically what you do with Dafny. I'm not very happy with this, not least of which is because it makes for an inferior developer experience in my opinion and because in general you are pretty limited in expressiveness of propositions.

Also it's kind of weird to be fixated on ATPs, as those are more or less a different level of abstraction from the language. You could develop an ATP for Bend.

More generally speaking, the largest, most well-known formal verification projects that verify actual code don't really rely on ATPs. SeL4 relies on explicit proof terms, CompCert relies on explicit proof terms, etc.

Silly question, but in Rocq, just for example, what does prevent you to fire `auto`, then, when it solves the goal, to just substitute it in your proof with the term that it constructed? Not calling you on BS, but genuinely interested in the problem

This significantly helps compile times, but will still end up with something far slower than Bend. What was I was talking about and presumably what LightMachine is talking about is how Bend is significantly more verbose than Rocq because even if you wrote out everything with terms, Rocq is still substantially slower than Bend, because Rocq relies a lot on implicit machinery (much more significant elaboration, implicit args, etc.) that slow down compilation.

>That is what makes Bend realistically 10x-100x faster than every alternative.

Do you have benchmarks which show this?

Hi!

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!

Hi! I'd like to know how bend2 differs from Hoare logic or Lean?

Speed.

> The checker file records 0.295 seconds for Bend and 36.177 for Lean on its 12,800-definition fixture. https://bend2.dev/notes/what-is-bend2/

I was with you until this.

> 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.