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."
> 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.
That rule doesn't mean it's illegal to move a piece that's pinned. It just means that it's illegal to move it to a square that would expose the king. For example a pawn that's pinned vertically can still push forward, it just can't capture diagonally.
That's why treating colloquial concepts like "pinning" as though they are rules in and of themselves is not really precise or productive.
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.
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.
> instead of thinking about how state transition you focus on what the program is allowed to perform
The state transition is what the program is or isn't allowed to perform. The state they're talking about in the invariant isn't the program state, it's the game state.
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.
doubtful, or at least not useful ones. Like, you could describe some invariant along the lines of "the position is winning for the side-to-move, iff there exists move, such that position' := ApplyMove(position, move) is losing for the (now other) side-to-move". But that's just restating minimax algorithm that people have known for 50 years.
As someone dabbling abit around chess engine development, I'm very often impressed by the many intricacies and observations made by people who pushed the envelope. It just doesn't sound plausible people wouldn't have discovered these killer invariants by now if they existed
I agree it's hard and non-obvious. If it wasn't then chess would have long been solved by now.
Let's start from the other end. Just a pawn and two kings. It's possible to describe some quite succinct rules for when that's a draw versus a win for the side with the pawn. Agreed? Club players know these by heart. You could write that doen as invariants. As long as the side with the pawn stays inside the "green zone" of the state space, there is nothing the other side can do to void mate. And vice versa, if the game is in the red zone and the other player manages to stay inside that red zone, there is nothing the side with the pawn can do to win. Those areas of the state space, green and red zones, can be described as invariants, in contrast to just enumerating them. It's very compact and can easily be checked by a machine that it's correct.
Now let's add a pawn. And another. And a rook perhaps. The more you add, the harder the condition is to describe, but we live in the age of billion-node-sized neural nets, we have the resources. Eventually you get all pieces on the board, and if the starting position satisfies the draw invariant, that's it. And likely the 960 freestyle chess positions too.
The well-known algorithms book Cormen et al. describes a lot of algorithms using loop invariants. I must say I never really liked this approach but I admit it makes things easier to reason about.
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):
So many of these invariants are redundant and so few of them encode any of the interesting rules of chess.
> 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.
The historical rules also left ambiguous promotion to the opposite color: https://chess.stackexchange.com/questions/8291/pawn-promotio.... This rule was clarified later to restrict to the same color.
> 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.
That rule doesn't mean it's illegal to move a piece that's pinned. It just means that it's illegal to move it to a square that would expose the king. For example a pawn that's pinned vertically can still push forward, it just can't capture diagonally.
That's why treating colloquial concepts like "pinning" as though they are rules in and of themselves is not really precise or productive.
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.
10 replies →
You can also pin a pawn to a queen, but the pawn can still legally move.
1 reply →
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.
3 replies →
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.
A nice read. I've been playing around with my own chess program and trying to implement a lot of chess variants like Double Chess and 7 Queen's Chess.
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
Correct. Also: https://www.learntla.com/
If you like this, you're probably gonna like this: https://en.wikipedia.org/wiki/Chessboard_complex
This is delightful. Thanks.
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.
> instead of thinking about how state transition you focus on what the program is allowed to perform
The state transition is what the program is or isn't allowed to perform. The state they're talking about in the invariant isn't the program state, it's the game state.
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.
doubtful, or at least not useful ones. Like, you could describe some invariant along the lines of "the position is winning for the side-to-move, iff there exists move, such that position' := ApplyMove(position, move) is losing for the (now other) side-to-move". But that's just restating minimax algorithm that people have known for 50 years.
As someone dabbling abit around chess engine development, I'm very often impressed by the many intricacies and observations made by people who pushed the envelope. It just doesn't sound plausible people wouldn't have discovered these killer invariants by now if they existed
I agree it's hard and non-obvious. If it wasn't then chess would have long been solved by now.
Let's start from the other end. Just a pawn and two kings. It's possible to describe some quite succinct rules for when that's a draw versus a win for the side with the pawn. Agreed? Club players know these by heart. You could write that doen as invariants. As long as the side with the pawn stays inside the "green zone" of the state space, there is nothing the other side can do to void mate. And vice versa, if the game is in the red zone and the other player manages to stay inside that red zone, there is nothing the side with the pawn can do to win. Those areas of the state space, green and red zones, can be described as invariants, in contrast to just enumerating them. It's very compact and can easily be checked by a machine that it's correct.
Now let's add a pawn. And another. And a rook perhaps. The more you add, the harder the condition is to describe, but we live in the age of billion-node-sized neural nets, we have the resources. Eventually you get all pieces on the board, and if the starting position satisfies the draw invariant, that's it. And likely the 960 freestyle chess positions too.
That king promotion rule sounds like it made the game more fun.
Screenshots of code? In 2026?...
That's how you know "principal research scientist" are true credentials. I'm sure the offline version is a postscript instead of pdf.
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
The well-known algorithms book Cormen et al. describes a lot of algorithms using loop invariants. I must say I never really liked this approach but I admit it makes things easier to reason about.