> 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.
> 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.
The point is that, logically, the first part of that rule (“expose the king”) is implied by the second part (“leave that king”), so the first part is redundant. You could simplify the rule to:
No piece can be moved that will leave the king of the same color in check.
And discovered check means that it is not sufficient to check the position of the piece you have moved, you also need to check the position of other pieces to see whether there is a new check.
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.
> 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.
Well, if a piece is pinned it's illegal to move it.
Rule 3.9.2: No piece can be moved that will either expose the king of the same colour to check or leave that king in check.
Unlike en-passant and castling, pinning and discovered checks are consequences of lower-level rules.
At the "Is this move legal?" level, they don't need unique rules of its own if the lower-level rules are specified correctly.
3.9.2: no piece can be moved if that exposes or leaves its own king in check.
That's a consequence of not being allowed to put yourself in check (by any means).
The only way to put yourself in check is by moving.
Did you mean putting your opponent in check? In chess, you are not allowed to put yourself in check.
You said “ That's a consequence of not being allowed to put yourself in check (by any means).” My point is that there are no other means.
The only action you can ever take in chess is moving.
You can also pin a pawn to a queen, but the pawn can still legally move.
You're both right, depending on whether you mean relative pin vs absolute pin.
The point is that, logically, the first part of that rule (“expose the king”) is implied by the second part (“leave that king”), so the first part is redundant. You could simplify the rule to:
No piece can be moved that will leave the king of the same color in check.
You should submit it to FIDE.
Pinning isn’t a rule, it’s just something that arises from other rules.
Also, pinning can happen with pieces that don’t include a king, which means you can just move out of the pin and expose whatever other piece.
It’s just a chess tactic, not a rule. It’s like saying a chess skewer is a rule too.
And discovered check means that it is not sufficient to check the position of the piece you have moved, you also need to check the position of other pieces to see whether there is a new check.
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."
Payments have a gargantuan amount of possible transitions and invariants that are far from trivial to encode.
Shameless plug: a code walkthru modeling the rules of chess, ment as an exercise/teaching functional programming (in Clojure):
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):
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.
I read these images of source code the same way as I read images of math formulas on Wikipedia: Not at all.
Anyone know what language is being used in the blogpost?
TLA+ i think
If you like this, you're probably gonna like this: https://en.wikipedia.org/wiki/Chessboard_complex
This is delightful. Thanks.
That king promotion rule sounds like it made the game more fun.
One king per color?
Screenshots of code? In 2026?...
side question, which CS class(es) teach about invariants?
Usually goes under Formal Methods: https://github.com/luigiapetre/Formal-Methods-Courses
There’s a book called Logic for Programmers: https://leanpub.com/logic#table-of-contents