Hacker News new | past | comments | ask | show | jobs | submit
> The only way to do that is to make your code provable. That again is only realistically doable using AI.

I think that LLMs actually cannot do this right now while people can?

Also there is a lot of defensive programming that has been left to application and runtime layers because of dated security models in our OS and permissions that are way too coarse. It's a lot easier to write a correct program when you don't have to check every path and do that perfectly when the permission system can ensure that no files that haven't been whitelisted cannot be read

My intuition is the opposite? The math results we are seeing lately are done with theorem provers. LLMs are getting very good at this and surpassing what humans have been able to prove. Verified code is traditionally very expensive and only applicable in niche areas when done by humans.
> LLMs are getting very good at this and surpassing what humans have been able to prove.

But if the reverse were true it would be impossible to prove. AI is trained on all of humanities solutions - LLMs stand on the shoulders of giants, not the other way around.

loading story #50372560
loading story #50370422
LLMs can, in principle, do everything humans can. And arguably more. "Right now" is how long? People are slow.

"Provable" essentially means, you have explicit operators acting on explicit states in an exhaustively defined way that preserves "truth", explicitly defined invariants.

A finite thing you can argue over deterministically.

Obviously, "you" there is an LLM, the machine your code is run on has to be defined in that very same exacting manner and so on.

That still isn't enough, you need abstraction, a hierarchy of categories that preserve your intent and accurately describe the problem space.

"Programming" then is solving an inverse problem over that hierarchy, filling in the blanks sensibly on your way down through the model hierarchy, all the way to atomic instructions your (proven) hardware understands.

Those layers of proper abstraction is what's largely missing currently. Or rather, is merely vaguely approximated.

All of which is to say: yes, the current state is a mess. Resolving that is far from easy.

But you really have no choice, that mess is transparent to large-enough LLMs. Security by obscurity only goes so far.

> But you really have no choice, that mess is transparent to large-enough LLMs.

It's transparent to large-enough LLMs given enough resources. Which is the thing that was always true. The difference now is that the level of resources is lower, so we're finding a bunch of things it wasn't previously economical to find.

But the cost still isn't zero. On top of that, the same LLMs are now generating enormous volumes of new code, which both nobody has verified to that level of exaction and nobody has even considered how it interacts with existing and other new code.

> Those layers of proper abstraction is what's largely missing currently. Or rather, is merely vaguely approximated.

This I can agree with, and my perspective would be that we have theoretical solutions with no ergonomics, and rely on unproven (as in formally proven/validated) mechanisms. WASM + capability passing is enough, but the WASM layer is still built on an OS or runtime that is not proven and you'll have a heck of a time trying to build a product on it

LLMs can't do a backflip. I can.
loading story #50370296
loading story #50372052
> LLMs can, in principle, do everything humans can.

I think narrowing the scope of this statement would better support your argument, as it is easily disproved in its current form.

> LLMs can, in principle, do everything humans can.

Oh yeah? slides baton Pick up that can, Clanker.

Jokes aside, I do want to see the first news of AI going out of its way to acquire and make use of actual currency and hiring a meat proxy. I don't even care what for, can be making paperclips.

loading story #50377948
https://bend-lang.com/

Folks are creating some interesting stuff in this space