wtf is lean64?

Lean 64 is a small first-person shooter game inspired by the classic game Doom, but with a twist: almost the entire game is written in Lean, a programming language normally used for mathematical proofs and formal verification rather than games. The author notes with some surprise that Lean turns out to be capable enough to build a real playable game in. The game runs in its own window and includes a title screen with three difficulty settings, a small two level campaign, and a fair amount of content for such an unusual experiment. Players can walk and strafe around 3D levels, aim with the mouse, sprint, fire weapons, open doors and switches, and check their progress on an in game map. There are two collectible weapons, a double barrel shotgun and a multi barrel chaingun, each with its own firing animation, sound, and recoil behavior. Combat includes multiple enemy types with basic artificial intelligence that can notice the player, chase them, attack up close or from range, and eventually die with visible effects like blood, sparks, and debris. The two levels end in an encounter with a stronger boss enemy. Along the way players can find hidden secret areas, pick up health and ammunition, and unlock progress using a collectible keycard, all tracked with an end of level results screen showing accuracy, kills, and score. Technically, the project separates the actual game logic, meaning things like physics, enemy behavior, camera movement, and menus, from the low level graphics and sound plumbing. The game logic itself is written entirely in Lean, while a small supporting piece of code handles opening a graphics window, talking to the computer's graphics hardware, and playing sound effects, since Lean on its own cannot do those platform specific tasks. All the visuals and sounds in the game are original and generated by the project itself rather than reused from Doom or any commercial game, since the author avoided using any copyrighted game data. To run it, you need to install a tool called elan, which manages Lean installations, and then use two build commands to compile and launch the game.