It does somewhat, or at least used to for a few months. Nowadays it kinda seems that the models have internalized something like TLA and are thinking in it in parallel to thinking in the language they’re writing, so it doesn’t help as much. This is all educated guesses from me, I’ve been telling models to do TLA back in the stone age around February and stopped seeing improvements when telling them to start with specs.
replyI’m however pretty sure that if you push a good model hard enough on a code base complex enough it’ll find stuff it wouldn’t have otherwise, the Specula folks have some experience with this.
A TLA+ spec defines both a model and properties (global invariants). How do you know that the properties the LLM specifies are the ones you care about?
reply