Show HN: Lean64 – 基于 Lean 4 的 Doom64 风格 FPS 游戏

Lean64 是一个实验性质的第一人称射击游戏，完全使用 Lean 4 编程语言实现。该项目由独立开发者 aouxwoux 创建，灵感来源于经典游戏 Doom 64，但并非其移植版或使用其版权数据，而是从零开始构建的原创原型。

游戏的核心功能包括完整的 Doom 风格体验：玩家可以使用 WASD 加鼠标进行移动、瞄准和射击，支持开门、切换武器、自动地图等操作。游戏包含两个关卡组成的迷你战役，玩家需要在其中对抗多种敌人，使用双管霰弹枪和转轮机枪等武器，并收集弹药、血包和钥匙来推进进程。敌人 AI 实现了警觉、追击、近战和远程攻击等行为，还包括一个独特的 Boss 战。

从技术角度看，Lean64 展示了 Lean 4 在游戏开发领域的潜力。游戏状态、AI、相机变换、网格构建和 HUD 合成均在 Lean 中实现，而底层渲染和音频则通过少量 C 代码与 Win32/OpenGL 交互。项目包含了软件光栅化器作为参考后端，并支持 GPU 深度测试和程序化纹理。开发者列出的大量功能清单涵盖了从基本的 3D 渲染、碰撞检测到复杂的粒子效果和音频调度等方方面面。

Lean64 目前仍处于早期开发阶段，未来的计划包括实现 WAD 读取器、BSP 遍历、精灵动画等，以接近源端口水平。所有资源（包括美术和音效）均为原创，项目采用 MIT 许可协议，源代码已托管在 GitHub 上。对于对游戏开发或函数式编程语言感兴趣的开发者来说，这是一个有趣的开源参考项目。