Comment by Animats

Now if we can get LLMs to do that, they might code better. Proofs are a lot of work, but might keep LLMs on track.