[grumbelbart]

Long-term this would be done using LLMs. It would also solve LLMs' code quality issues - they could simply proof that the code works right.

[photonthug]

> simply proof that the code works right

Combining LLMs + formal methods/model checkers is a good idea, but it's far from simple because rolling the dice on some subsymbolic stochastic transpiler from your target programming language towards a modeling/proving language is pretty suspect. So suspect in fact that you'd probably want to prove some stuff about that process itself to have any confidence. And this is a whole emerging discipline actually.. see for example https://sail.doc.ic.ac.uk/software/

[codebje]

Maybe very long term. I turn off code assistants when doing Lean proofs because the success rate for just suggestions is close to zero.