Lean64 は、Lean 4 プログラミング言語で完全に実装された実験的な一人称視点シューティングゲームです。開発者の aouxwoux によって作成され、古典的なゲーム Doom 64 からインスピレーションを得ていますが、その移植版ではなく、ゼロから構築されたオリジナルのプロトタイプです。
ゲームプレイは、WASD とマウスを使った移動、射撃、ドアの開閉、武器の切り替え、オートマップといった完全な Doom スタイルの操作をサポートしています。2つのレベルからなるミニキャンペーンでは、複数の敵と戦い、ダブルバレルショットガンやチェインガンなどの武器を使用し、弾薬、回復アイテム、鍵を収集します。敵 AI は警戒、追跡、近接攻撃、遠距離攻撃を実装し、ボス戦も含まれています。
技術的には、Lean64 は Lean 4 のゲーム開発への応用可能性を示しています。ゲームの状態、AI、カメラ変換、メッシュ構築、HUD 合成はすべて Lean で記述され、低レベルのレンダリングとオーディオは最小限の C コードを介して Win32/OpenGL と連携します。プロジェクトにはソフトウェアラスタライザがリファレンスバックエンドとして含まれ、GPU 深度テストとプロシージャルテクスチャもサポートしています。開発者による詳細な機能リストには、3D レンダリング、衝突検出から複雑なパーティクルエフェクト、オーディオスケジューリングまで、幅広い要素が網羅されています。
Lean64 はまだ初期開発段階にあり、今後のマイルストーンとして、法的に供給された WAD リーダー、BSP トラバーサル、テクスチャアトラス、スプライトアニメーション、より大規模なキャンペーンの実装が計画されています。すべてのアセットはオリジナルであり、プロジェクトは MIT ライセンスのもとで GitHub に公開されています。関数型プログラミング言語に興味のあるゲーム開発者にとって、貴重なオープンソースの参考資料となるでしょう。