Hacker News Reader

Comment by alerighi | Hacker News Reader

> That again is only realistically doable using AI

The opposite. The amount of bugs that I've seen AI add to software is tremendous, some bugs are things that even a 18 years old that starts working as a developer right after school wouldn't do.

Also they are unable to fix them, if you ask them to fix a bug they probably introduce 3 other more, and so on, and you arrive quickly at the point that the code is a mess of spaghetti that needs to be rewritten completely (by a human, this time).

On the opposite side AI is good at finding bugs, so I use it more as an advanced linter that tells me if I'm doing something wrong.

View on HN

You’re describing vibe coding and GP is describing systems for proving correctness.

If you ask an AI to generate a novel math proof, it will inevitably produce garbage. If you give it the tools to do this (e.g. Lean), evidence is that it can in fact generate meaningful proofs.

To the extent that we cannot prove software correct, this is probably largely a tooling problem.

“tooling problem” makes it sound trivial, its a tooling problem like building a quantum computer is a tooling problem. Ie something that probably won’t be solved in our lifetime

> something that probably won’t be solved in our lifetime

If you told me five years ago that AI would eventually be generating novel math proofs, I probably would’ve said that it’s not happening in my lifetime. And yet here we are.

I don’t know what it looks like to get to fully provable code, but I don’t see that it’s fundamentally impossible in my lifetime. Especially depending on scope. Will an entire operating system and everything on it be fully proven correct in my lifetime? Maybe not. Could the authentication stack for a product be entirely proven correct? Sure. I can’t believe that.

> If you told me five years ago that AI would eventually be generating novel math proofs, I probably would’ve said that it’s not happening in my lifetime. And yet here we are.

A single PC can solve a very complex simulation model in seconds, something that would require years using humans to do. Same as solving a very complicated maze. So if coupling a text generator with a proof verifier is now capable of coming up with a proof, I’m not particularly surprised. But given the cost, and the actual usefulness of the proof, I’m not particularly excited either.

But code is not a closed system, even if we do prove a lot of the internal mechanism, we still can’t know the input (noise), and whether the axiomatic foundation will hold. That’s the reason people don’t bother. The theory of computation is just too loose in its constraints. You just write enough tests to catch egregious errors.

> But code is not a closed system

Code is absolutely a closed system.

"Software" might not be, and definitely not software systems -- but code can have each part of it atomically proven to be correct, assuming you test it with a sufficiently complex simulation model (which you've already granted is within the possibilities for LLMs).

Prove all the code in the software system correct, then prove their interactions are correct, and you've achieved your goal.

(I won't claim this is inevitable with the current tools, but it's at least within the realm of possibility)

> we still can’t know the input (noise)

Doesn't matter. Just like you can prove something is true for all numbers, you can prove something is true for all possible inputs.

You should try AI out, it’s a lot more capable than it was when most people formed their opinion a few years ago.

I use it every day

What model are you talking about when you say this? "AI" is not one thing, and if you think frontier models are at all comparable to a typical 18yo SWE, you've never actually worked with one of those two.

Reply on news.ycombinator.com