GoKawiilChess 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.
It is a concurrent system, but with a very specific kind of concurrency: interleaved execution. More specifically, taking turns: white, then black, then white.
You know what we do with concurrent systems here? Here we model them, and we distill their invariants.
Here is some setup definitions first.
In a CS or math paper, if you write "Section 2: Model and Problem" well enough, the rest of the paper writes itself. With this setup you can sort of see what the actions will be.
In fact, forget about the actions. Let's look at some invariants.
... continue reading