[comex]

Well, for one thing:

> Decline to buy: property stays with bank (auction abstracted out)

Ignoring an entire game mechanic is really stretching the definition of “abstracted out”…

Also, at the bottom it defines a “Liveness: someone eventually wins” property which I believe cannot be proven. Monopoly doesn’t have any rules forcing the game to end eventually. There is only a probabilistic guarantee, and even that only applies if the players are trying to win; if the players are conspiring to prevent the game from ending then they’re unlikely to fail.

[tombert]

Yeah, I finally started thoroughly reading it this morning, and the lack of a guarantee of winning was one thing that stuck out to me as well.

I do think Claude is getting better at this stuff but I will probably keep writing the specs myself for now.