this post was submitted on 11 Aug 2026
-1 points (42.9% liked)

Programming

28138 readers
318 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

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
 

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
[–] thingsiplay@lemmy.ml 5 points 1 week ago

So just write more tests and a Test-Driven-Development (TDD)? Someone has to engineer these tests too. How does the simulation software (which itself needs to be developed and updated) know all behaviors of a system, that is relevant to it? You basically ask if we someday could have a magic box that does all of that for us.