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