Lean 4は、HaskellやOCamlと系譜を同じくする関数型プログラミング言語です。主にソフトウェアの正当性を数学的に検証するためのツールである「証明アシスタント」として知られていますが、近年では汎用的なアプリケーション開発のための実行可能な環境へと進化しています。この言語の標準ライブラリには現在HTTPサーバーが含まれており、コミュニティ主導のライブラリのエコシステムが拡大することで、PostgreSQLドライバ、暗号化、HTMLレンダリングなど、現代のWebアプリケーションに必要なインフラを提供しています。
これらの能力をテストするために、ある開発者はフルスタックの実装をベンチマークするために使用される有名なリファレンス・アプリケーション（Mediumのクローン）である「RealWorld」を構築しました。このプロジェクトでは、低レベルの接続処理のための`Std.Http`、型付きパラメータでAPIルートを定義するための`lean-routing`、およびデータベース操作のための`leanpostgres`といういくつかの主要なコンポーネントを利用しています。注目すべき設計上の選択として、従来のテンプレートを使用するのではなく、`lean-html`を使用してページを通常のLean関数としてレンダリングしています。フロントエンドのインタラクティブ性のために、プロジェクトではDatastarのSDKである`datastar-lean`を採用しており、これによりサーバーは最小限のフロントエンドビルドステップでページを動的に更新できます。結果として得られたバックエンドの実装は非常に簡潔で、合計1,033行のコードとなっており、TypeScript、Go、C#によるいくつかの一般的な実装よりも短くなりました。
開発者は、Lean 4がフルスタックの要件を処理できることを示すためにRealWorldプロジェクトを使用しました。
このプロジェクトは、Lean 4がフルスタックの要件を処理できることを証明する一方で、本番環境への準備状況と形式的検証に関する特定のトレードオフを浮き彫りにしています。現在のLean HTTPサーバーには既知のパフォーマンス上の制限があり、言語の急速なリリースサイクルによって時折依存関係が壊れることもあります。さらに、Leanはコードを形式的な仕様から導出し、すべてのステップを数学的に証明する「構成による正当性」を可能にしますが、開発者はRealWorldの仕様は部分的にしか形式化されていないと指摘しました。例えば、アプリはURLの「slug」が正しく構成されていることを証明できますが、これはその妥当性の数学的証明とセットでバンドルされているためです。一方で、より広範なアプリケーションの動作は依然として従来のテストに依存しています。このプロジェクトは、Lean 4が高品質で検証されたコードへの道を提供する一方で、現在は重要なロジックのための形式的証明と、一般的な機能のための標準的なテストのバランスが必要であることを示唆しています。