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."

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):

  (defn expand-pmove-for-rook [pmove]
    (->> pmove
      (expand-pmove-dirs [↑ ↓ ← →])
      (pmoves-discard #(or (pmove-on-same-player-piece? %)
                           (pmove-changed-direction? %)))
      (map pmoves-finish-capturing-opponent-piece)
      (pmoves-finish-and-continue))))

> 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.

So many of these invariants are redundant and so few of them encode any of the interesting rules of chess.

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.

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.

If you like this, you're probably gonna like this: https://en.wikipedia.org/wiki/Chessboard_complex

Anyone know what language is being used in the blogpost?

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.

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.

That king promotion rule sounds like it made the game more fun.

Screenshots of code? In 2026?...

side question, which CS class(es) teach about invariants?