Comment by mccoyb | Hacker News Reader

Comment by mccoyb | Hacker News Reader

@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?

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

If you're going to insinuate that the author of Bend2 doesn't understand PLs and formal verification, you should do so with some proof and not a hot take dunk.

I think it's fine to critique the language and the approach without criticizing the author and I hate that this site has become Tech Drama News, like the worst parts of Twitter.

Yes, I didn't realise how much it comes off as a critique of the author personally when I wrote it. I have added a note to that effect to the top of the article.

conversations on this site about formal methods are currently absolute cess pits of dunning kruger and confidently stated yet highly misinformed takes from those with close to little experience in the field.

I think sadly all big conversations on this site are like this these days. It didn't used to be like that sadly. Z3 and some early Lean threads used to be great.

Perhaps because their concerns are different? Similar reasoning: "why invest in dependently typed languages over SMT solvers? SMT solvers are automatic, and it is way easier to add annotations to my programs"

The answer is that these technologies are not universal in trade off space.

Of course, if you can have an LLM prove something by dispatch to an SMT solver ... you want to do that (and, indeed, LLMs do sometimes do this even when working on Lean proofs)

But the space of statements that you can prove using verification with SMT is smaller than dependently typed systems.

Also, Ada/SPARK are very good and robust -- they've been around for ~50 years ... but there's been a significant amount of work in formal verification since then, right? I would be more clear that Ada/SPARK are state-of-the-art for "mission critical software" (and have been for many years), but there's been a lot of research work in formal verification of low level programming since then (Low*, for instance)

I'm assuming you have not spent a lot of time trying to prove stuff about non trivial programs if the trade offs between SMT based approaches and interactive theorem provers are not clear to you.

SMT solvers are highly automated, but very opaque and hard to debug. Interactive theorem provers can scale to larger problems and harder properties at the cost of increased manual proof burden. The ever increasing ability of llms to write proofs in a theorem prover has in recent years tipped the balance significantly towards preferring itp based approaches over pure SMT ones. The current state of the art for program verification is probably a mix of llm and traditional (tactics, SMT, etc.) proof automation inside an itp.

ATPs go quite a bit beyond what a SMT solver can do, however you're not stuck with just using ATPs when they are supported. You can still allow for proofs to be manually written with an ATP doesn't work, and in fact SPARK allows for this with Rocq.

Most of what I have to prove is floating-point code where a manual proof is too much of a headache to ever attempt though.

You clearly don't know shit about the whole topic, yet attack an open-source project's author who wasn't even the one posting his own project..

> Why would we want the tradeoff where the LLM has to write significantly more code and where the specification needs to be more complicated? If the author is aware of the state of the art then I think they made a poor choice, but that's not the point.

Because code is trivially cheap now. LLMs churn out a shitton of code at pennies, and as technology improves their per-line cost will continue to decrease. A proof has to be written once and it's never read again. It's only important property is that it is machine-verifiable - from then on only the signature matters. Meanwhile speed of compilation matters, so an obvious tradeoff was made by the author.

> my general point is about how people will vibe-code a solution without an understanding of the field, leading to worse results than if they spent a little while understanding the field and then vibe-coded their thing.

This is clearly not the case here, and even if it were, it's still a better thing than vibe-blogging clickbait shit with extra amount of Dunning–Kruger. Calling out an author who clearly works in the field for a decade or more for not knowing the topic...

Reply on news.ycombinator.com