Lean 4でRealWorldアプリを構築、テストスイートを全通過
I built the RealWorld app in Lean 4
Lean 4はHaskellやOCamlの系統に属する関数型言語で、証明支援系として知られている。標準ライブラリにHTTPサーバーが加わり、コミュニティがPostgresドライバやHTMLレンダリングなどのライブラリを整備しつつある。著者はMediumクローンのRealWorldをLeanで実装し、公式のAPIテストとウェブサイトテストを通過させた。バックエンドは1,033行で比較した4実装中最短。ただしHTTPサーバーの性能限界やライブラリの若さといった課題も正直に述べている。
Leanは各証明が正しいことをチェックするが、その定理が本当に必要なことを述べているかまではチェックできない。
- saviorand
Lean 4が証明だけでなく、日常的なWebアプリにまだ使えるのか知りたかったので、RealWorld（Mediumクローン）をフロントエンドも含めてDatastarを使ってLean 4で構築してみました。新しいライブラリのおかげで、今なら実現可能なようです。この記事ではその経験について説明しています。
- hiAndrewQuinn
これは素晴らしいニュースです。昨年、汎用ソフトウェア開発のためにLeanを調べたところ、ライブラリの面でかなり不足していることが分かりました。ですから、例えばleanpostgresが実用的に使えるというニュースは大きな前進です。
- solomonb
Lean4の秘密は、実は優れたプログラミング言語だということです。いわばスーパーHaskellのようなものです。実際、証明チェッカーとしてよりもプログラミング言語としての方が好きです！依存型は形式検証に加えて通常のプログラミングにも素晴らしいです。証明チェックに関しては、私はむしろAgdaの方が好みです。