8 ms·
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.
by grumbelbart 1y ago
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.
- teiferer 1y ago[dead]
- codebje 1y agoMaybe very long term. I turn off code assistants when doing Lean proofs because the success rate for just suggestions is close to zero.
- photonthug 1y ago> 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/ https://sail.doc.ic.ac.uk/software/