Comment by benreesman

If you combine models/agents with formal systems, you can get them to come back when they're in a corner today: https://gist.github.com/b7r6/b2c6c827784d4e723097387f3d7e1d8...

This interaction is interesting (in my opinion) for a few reasons, but mostly to me it's interesting in that the formal system is like a third participant in the conversation, and that causes all the roles to skew around: it can be faster to have the compiler output in another tab, and give direct edit instructions: do such on line X, such on line Y, such on line Z than to do anything else (either go do the edits yourself or try to have it figure out the invariant violation).

I'm basically convinced at this point that AI-centric coding only makes sense in high-formality systems, at which it becomes wildly useful. It's almost like an analogy to the Girard-Reynolds isomorphism: if you start with a reasonable domain model and a mean-ass pile of property tests, you can get these things to grind away until it's perfect.