Comment by LightMachine | Hacker News Reader

Comment by LightMachine | Hacker News Reader

Parent Full thread

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.

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

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.

Reply on news.ycombinator.com