Programming

28103 readers

178 users here now

Welcome to the main community in programming.dev! Feel free to post anything relating to programming here!

Cross posting is strongly encouraged in the instance. If you feel your post or another person's post makes sense in another community cross post into it.

Hope you enjoy the instance!

Rules

Follow the programming.dev instance rules
Keep content related to programming in some way
If you're posting long videos try to add in some form of tldr for those who don't want to watch videos

Wormhole

Follow the wormhole through a path of communities !webdev@programming.dev

founded 3 years ago

MODERATORS

snowe@programming.dev

Ategon@programming.dev

UlrikHD@programming.dev

bugsmith@programming.dev

Spyro@programming.dev

AI and formal verification (lemmy.ml)

submitted 4 days ago by maegul@lemmy.ml to c/programming@programming.dev

4 comments fedilink hide all child comments

Realistically, how much more does AI for coding have to get out of leaning and training more for formal verification (with eg Lean, Rocq etc and their interop with mainstream langs)

If AI hasn’t really pursued this strongly, then maybe a good amount, right?

I can imagine a scenario where you no longer review the code but a simulation of all the behaviours of the system, perhaps before any code has been written, and then you can trust the output will have accordingly …?

What practical limits of formal verification are there for this?

And for the anti AI folks, I’m anti AI too and I don’t use it or want to use it at all. I’m thinking about the future here.

you are viewing a single comment's thread
view the rest of the comments

[–] hendrik@palaver.p3x.de 3 points 3 days ago* (last edited 3 days ago)

Yeah, I think so as well. Limit of formal proofs is reality. Even seemingly simple stuff is super complex and interacts with a plethora of other things. And your conclusion will only ever be as good as the model / specifications you put in. When doing the maths on a crypto algorithm... Have you thought of people whipping out their multimeter to probe the power consumption of the CPU and subsequently work their way back to the secret? Have you favored in everything else that exists on the world, or potentially could exist? If not, your result just won't line up with reality as it is out there.

Formal proofs are very, very good if you made up the parameters. But good luck formalizing reality once it gets down to applied stuff... I mean it's still useful and helps make things better. But it's not like airplane systems don't fail anymore after we've come to do formal proofs on the subsystems. It's just too complex and the real world is involved.