> Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate.
Nit: Pinning and the discovered check are not really rules, but rather names of tactics.
I can't wait to show this to my manager next time he asks why it's taking three weeks to build a simple CRUD app.
"Look, if this guys TLA+ logic struggles to model a 1,500-year-old game without crying over a French pawn-capture rule, you can't expect me to integrate Stripe billing without a few state invariant violations."
While I think everything written in this post is correct, what really is starting bothering me is this over-focus/attention on data even when what you want to express is behavior, let me explain:
The post talks about "transition invariants" that should be somehow different from "state invariants" yet it describe them as:
> These are predicates over a <<state, next-state>> pair ...
i.e. it still is about state, but I find it much more useful to focus on behavior so instead of thinking about how state transition you focus on what the program is allowed to perform, regardless of the underlying data structure.
What I mean is that I'd like the code to tell me why a certain piece can't do such move instead of why it cannot transition it's position to another position and basically dumping its state in my head and there I have to execute the program myself.
> Chess is a lot trickier than it looks. It has so many rules: castling, en passant, pawn promotion, pinning, the discovered check, and the deadlock case of stalemate.
As a kid playing chess with other neighborhood kids back in the day, absolutely none of us even knew about the en passant rule. My first exposure around the same time was completely by accident thanks to a passing reference in a CRPG called Betrayal at Krondor. It comes up in a story about a game that nearly costs an innkeeper her establishment when she loses because of a move she didn’t even know existed.
If I play a casual game with someone who doesn’t know about en passant and they make a move that opens them up to it, I don’t attempt to take the piece, but I do point it out to them and recommend we use the rule in future games.
This is just the beginning. You could create more and more advanced invariants. And I am sure that this could be a way to "solve" chess, i.e., prove that it's a draw with perfect play.
> The player’s choice is not restricted to pieces that have been captured previously
I grew up playing chess but my grandfather always insisted that pawns could only be promoted to captured pieces so when I played him we had to play a that variant.
I suspect this came from players not having extra pieces with their chess sets.
That and just avoiding the obvious advantage of promoting every piece to a queen every time. Puts more constraint on the game which usually makes for more interesting play
> apparently it wasn't until 19th century that people made clear that you couldn't promote a pawn to a King, surprising an attempted checkmate by responding Le roi est mort, vive le roi!
That's the coolest thing ever though, why would you ban such a move, where's the rule of cool when you need it most?
> It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white.
"Chess is a game of imperfect information, but with a very specific kind of imperfectness: fully available information. More specifically, ever single information is visible: you see all your opponents' pieces and he sees all yours, you see how much time he's got left, and he sees how much time you have left".
Who knew it? Chess is actually a concurrent game of imperfect information: with that definition, it's not unlike a real-time strategy game like Warcraft 3.
24 comments
[ 2.9 ms ] story [ 39.3 ms ] threadNit: Pinning and the discovered check are not really rules, but rather names of tactics.
"Look, if this guys TLA+ logic struggles to model a 1,500-year-old game without crying over a French pawn-capture rule, you can't expect me to integrate Stripe billing without a few state invariant violations."
The post talks about "transition invariants" that should be somehow different from "state invariants" yet it describe them as:
> These are predicates over a <<state, next-state>> pair ...
i.e. it still is about state, but I find it much more useful to focus on behavior so instead of thinking about how state transition you focus on what the program is allowed to perform, regardless of the underlying data structure.
What I mean is that I'd like the code to tell me why a certain piece can't do such move instead of why it cannot transition it's position to another position and basically dumping its state in my head and there I have to execute the program myself.
https://neuroning.com/boardgames-exercise/notebooks/walkthro...
The implementation makes it really easy to add new piece types or rules. For example, here's the full logic for rooks (sans castling):
As a kid playing chess with other neighborhood kids back in the day, absolutely none of us even knew about the en passant rule. My first exposure around the same time was completely by accident thanks to a passing reference in a CRPG called Betrayal at Krondor. It comes up in a story about a game that nearly costs an innkeeper her establishment when she loses because of a move she didn’t even know existed.
If I play a casual game with someone who doesn’t know about en passant and they make a move that opens them up to it, I don’t attempt to take the piece, but I do point it out to them and recommend we use the rule in future games.
I grew up playing chess but my grandfather always insisted that pawns could only be promoted to captured pieces so when I played him we had to play a that variant.
I suspect this came from players not having extra pieces with their chess sets.
That's the coolest thing ever though, why would you ban such a move, where's the rule of cool when you need it most?
"Chess is a game of imperfect information, but with a very specific kind of imperfectness: fully available information. More specifically, ever single information is visible: you see all your opponents' pieces and he sees all yours, you see how much time he's got left, and he sees how much time you have left".
Who knew it? Chess is actually a concurrent game of imperfect information: with that definition, it's not unlike a real-time strategy game like Warcraft 3.
Who would have guessed it?
99.9% chance you could have solved this in a couple of hours with some ifs and loops