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 上。對於對遊戲開發或函數式編程語言感興趣的開發者來説，這是一個有趣的開源參考項目。