This is a list of cool games related to computer science that you might not know about.
Well-Known Games
Zachtronics games
Purchased on Steam/GoG/Itch.io: https://www.zachtronics.com/
Various games about programming (or similar) under harsh constraints. The older ones (SpaceChem, TIS-100, SHENZHEN I/O) are harder than the more recent ones (Opus Magnum, EXAPUNKS)
Nandgame
Free to play: https://nandgame.com/
Build a computer from scratch through clicking and dragging by using only NAND gates and things you previously built out of NAND gates. It holds your hand throughout the entire journey by giving you a series of self-contained puzzles where you’re only allowed to use blocks you constructed in previous levels.
Virtual Circuit Board
Purchased on Steam: https://store.steampowered.com/app/1885690/Virtual_Circuit_Board/
Just a logic circuit sandbox… kind of. Unlike Nandgame it does not hold your hand at all, but is still efficient enough to allow you to implement a whole computer in there and even comes with the ability to write assembly for your own computer, so building your own computer can be considered one of the goals of the game. Consider playing this if after you completed Nandgame you wish you felt a bigger sense of accomplishment.
Gladiabots
Purchased on Steam: https://store.steampowered.com/app/871930/GLADIABOTS__AI_Combat_Arena/
Program bots to fight in a virtual arena using a flowchart-like programming language. The limitations of the language contribute to the amount of creativity needed to make a decent bot, as well as decreasing the barrier to entry.
Nicher Games
Incredible proof machine
Free to play: https://incredible.pm/
A game about proving things using intuitionistic logic. It has a very neat graphical interface that’s way easier to get into than a traditional proof description language like Coq or Lean
The game comes with no tutorial, so here's some things to get you started
- On the level select menu, everything above the line is things you are given as starting fact (“the givens”) and everything below the line is things you must prove using the givens (“the targets”)
- Once you’re in a level, the givens are on the left and the targets are on the right. You can connect givens (aka. facts) to the targets or to logical blocks to construct more complicated facts.
- Blocks correspond to logical axioms which you can chain into deductions. Supply their inputs with things that are true and the outputs will also be true.
- “A→B” means “if A is true then B is also true”. Can be thought of as a function that takes a proof of A and gives a proof of B.
- This is reflected in both how it’s used (using an A and an A→B you can get B) and the way it’s constructed (the → construction logic block is essentialy “I’ll give you an A, if you then use it to give me a B then that means A→B”)
- ⊥ (called “bottom”) is a value representing logical contradiction.
- A→⊥ is a way of saying “not A”, because if you’re given both A and A→⊥ you get ⊥
- The principle of explosion can be used to obtain any statement whatsoever from ⊥, which is useful during case analysis
- (A→⊥)→⊥ (aka. “not not A”) is not initially equivalent to A, it’s only when you’re given the principle of excluded middle (the TND block) that the equivalence can be proven
- Some of the ∀ (forall) and ∃ (exists) blocks are very similar, with the main difference being what variables they expect. An input/output variable called
ycorresponds to any variable you want, whereas a variable calledccorresponds to a brand new variable created by the logical block with you specifically must use during your proof.
Natural numbers game
Free to play: https://adam.math.hhu.de/#/g/leanprover-community/nng4
Again a game about proving things, but this time in Lean. I’d recommend playing the incredible proof machine first since Lean is not the most pleasant thing to write.
Deadlock empire
Free to play: https://deadlockempire.github.io/
Short game about commonly found mistakes in imperative multithreaded code. Does not involve writing code. Accessible even to people who’re still learning about multithreading.
Graphomata
Free to play: https://graphomata.com/game/play-online.html
Game about traversing and modifying graphs using only pointers to vertices. Involves writing code in a graphical language. Accessible even to people who’ve never written code.
ABI-DOS
Free to play: https://store.steampowered.com/app/2180700/ABIDOS/
A zach-like about moving numbers around to implement various operations. Prime Mover is very similar to this.
ComPressure
Purchased on Steam: https://store.steampowered.com/app/1528120/ComPressure/
A zach-like about designing circuits out of pipes and valves. Previous solutions are used when building future solutions, and slight errors in your earlier solutions accumulate on top of each other so optimization is important for correctness.
Bombe
Purchased on Steam: https://store.steampowered.com/app/2262930/Bombe/
Game about writing your own minesweeper puzzle solver. The challenge comes from having to write it in a very restricted language.
I’d consider this game a very good “legacy codebase simulator”; Two hours in and I already had a bunch of rules in the list that needed deprecating as they were already replaced by better rules. It wasn’t that long in that I had the urge to just delete everything and start writing rules from scratch.
CTFs
OverTheWire
Free to play: https://overthewire.org/wargames/
A bunch of beginner-level CTFs. “Bandit” is about teaching you basic linux shell commands, while the games after it teach basic web security, ciphers, etc.
Microcorruption
Free to play: https://microcorruption.com/
A CTF game about reverse-engineering locks. Read the assembly code of the lock, figure out its flaw(s), then type in a valid password. Surprisingly accessible for what it is. I’d say it serves as a great middle ground between the easy CTFs and the serious ones, as it still involves assembly but it does not involve learning how to use related archaic tooling.
Smash The Stack
Free to play: https://www.smashthestack.org/main.html
Even the “easy” CTFs on here are rather hard. Good luck!
Other cool things that aren’t really games:
- https://olus2000.pl/concat_eval - A sandbox for describing and evaluating concatenative calculus variants (the site has a readme that’s more descriptive than this, go read it for an explanation of what a concatenative calculus is)
- http://logitext.mit.edu/main - A click-based proof assistant for sequential calculus
- https://click-and-collect.linear-logic.org/ - A click-based proof assistant for linear logic
- https://homotopy.io/ - A category theory proof assistant that can visualize string diagrams