alt Hacker NewsClaude has certainly been getting better with TLA+. It's not perfect yet but for laughs I got it to model the rules of Monopoly last night [1]. I haven't done any exhaustive checking on it yet, but it certainly looks passable.
It is pretty impressive at how good it's gotten at this, in a relatively short amount of time no less. I still usually write my specs by hand, but who knows how much longer I'll be doing that.
Replies
It looks quite complicated and I have no idea what it is doing. Obviously, since I don't know about TLA+. But what about someone who knows TLA+? It still seems hard to make sure it is valid. And it's just for a relatively simple game.
> I haven't done any exhaustive checking on it yet, but it certainly looks passable.
isn't that exactly the kind of fails LLMs do the most? first-glance-passable nonsense?
What's the advantage of provable correctness if it's apparently not easy to prove even for people who understand TLA+? I'm not trying to be a party pooper, just curious.
Isn't logical incorrectness less of a problem in software than failures of imagination or conscientiousness in modeling the domain?