This is a list of cool games related to computer science that you might not know about.
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.
Nandgame
Free to play: https://nandgame.com/
Game about constructing a rudimentary processor purely out of nand gates through clicking and dragging.
Bombe
Can be bought 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)
- https://homotopy.io/ - A category theory proof assistant that can visualize string diagrams. It’s category theory so I still do not understand any of it, but it’s cool.