プログラミング

Lean 4でRealWorldアプリを構築した

I built the RealWorld app in Lean 4 (leangineer.com)

81 pointsby saviorand2026年10月15日10 コメント

要約

この記事では、関数型言語であり証明支援系でもあるLean 4を用いて、Mediumクローンである「RealWorld」アプリケーションを完全に構築した事例を紹介します。Lean 4のエコシステムが成長し、HTTPサーバー、データベース、フロントエンドレンダリングなどのライブラリが利用可能になったことで、実用的なWebアプリケーション開発が可能であることを実証しています。筆者は、Lean 4の実装が他の言語よりも短く、生産性やコードの信頼性についても考察しています。

全文翻訳

Lean 4でRealWorldアプリを構築した

［画像: Leanによってサーバーサイドでレンダリングされたホームページ。］

図1. Leanによってサーバーサイドでレンダリングされたホームページ。

1 はじめに

Lean 4は、HaskellやOCamlと同じ系統の関数型プログラミング言語です。多くの人はそれを証明支援システムとして認識しています。最近では、その標準ライブラリにHTTPサーバーも追加されました。コミュニティは、Postgresドライバー、暗号化、HTMLレンダリングなど、通常のアプリに必要な他のライブラリも作成しています。

では、Leanで実際のWebアプリを構築することは可能なのでしょうか？それを調べるために、私はRealWorldをLean 4で構築しました。RealWorldは有名なリファレンスアプリで、APIとウェブサイトの両方に公式テストスイートが付属するMediumのクローンです。私のバージョンは、フロントエンドを含め、すべてLeanで書かれています。フロントエンドはインタラクティブ性のためにdatastar-leanを使用しています。コードはGitHubで公開しています。

この記事は、主に面白さと構造の明確さを保つために、数学論文のように記述しました。以下で説明する内容のほとんどは、どの言語でも行うであろう通常のエンジニアリングです。実際に証明されている数少ない部分は、命題としてマークされています。Leanは、コードがビルドされるたびにそれらの証明をチェックします。

2 存在

最初の疑問は、LeanでRealWorldアプリを構築できるかどうかです。テストスイートは、それをチェック可能なものに変換します。

定義1. RealWorld実装とは、RealWorldのAPIスイートとそのウェブサイトスイート1をパスするプログラムである。

定理1. LeanにはRealWorld実装が存在する。

証明は、それを構築することです。テストスイートは、それが何をしなければならないかを定義します。APIテストはHTTPリクエストを送信し、返ってきたJSONをチェックするため、サーバーが必要です。それらの回答のデータは、リクエスト間で保持される必要があるため、データベースが必要です。ウェブサイトテストは、実際のブラウザでサイトを操作するため、サーバーはページをレンダリングする必要もあります。

構成1（サーバー）。Leanの標準ライブラリには、4月以来HTTPサーバーStd.Httpがあります。これは、低レベルの接続処理をすべて担当してくれます。そのサーバーの上に、lean-routingを使用してAPIのルートをテーブルで宣言しています。各ルートは、型付きパラメータを持つパスを持ち、独自のハンドラーを取得します。以下のコードの←はawaitと読みます。

route_table Api
  [ ...
    comment := "/api/articles/:slug:String/comments/:id:Nat",
    ... ]

def deleteComment (env : Env) (slug : String) (id : Nat) : Handler := fun req => respond do
  Service.deleteComment env (← requireUser env req) slug id
  noContent

def routes (env : Env) : List (Route Result) := 
  [ ...
    .delete patterns.comment (deleteComment env),
    ... ]

このハンドラーはコメントを削除します。requireUserでユーザーのログイン・トークンをチェックし、サービスレイヤーを呼び出してコメントを削除し、204 No Contentで応答します。ウェブサイトは同じサービスレイヤーを呼び出すため、まったく同じルールに従います。他のすべては、どの言語でもそうであるように、ライブラリから取得されます。

JSONにはlean-json
パスワードをOpenSSLのscryptでハッシュするにはlean-libcrypto
ログイン・トークン（JSON Web Tokens）にはlean-jose
CORS、Cookie、静的ファイルにはlean-middleware

構成2（データベース）。データはPostgresに格納されます。私はleanpostgresを通してそれにアクセスします。これはPostgresのCクライアントをラップし、接続プールを維持します。SQLはコード内に直接記述します。返ってくる各行はLeanの構造体に変換されます。

def userByEmail (db : Conn) (email : String) : IO (Option UserRow) := do
  first (← db sql!"SELECT id, username, email, password_hash, bio, image FROM users
                     WHERE email = {email}")

sql!内の{email}はクエリパラメータになり、PostgresはSQLテキストとは別にそれを受け取ります。そのため、ユーザー入力がSQLとして実行されることはありません。データベーススキーマはプレーンなSQLで、サーバー起動時にleanmigrateが適用します。

構成3（ウェブサイト）。ページはlean-htmlでサーバーサイドでレンダリングされます。HTMLは通常のLean関数として記述されているため、テンプレートはありません。これは、コメントと、あなたが書いた場合はゴミ箱アイコンを表示するコードです。

def commentCard (viewer : Option Db.UserRow) (slug : String) (c : Db.CommentRow) : Node .flow :=
  let delete : List (Node .phrasing) :=
    if viewer.any (·.id == c.authorId) then
      [ span [ i [] { class_ := "ion-trash-a" } ] { class_ := "mod-options" }
          [onClick (action "delete" (Site.links.comment slug c.id.toInt.toNat))] ]
    else []
  div [
    div [ p [ c.body ] { class_ := "card-text" } ] { class_ := "card-block" },
    ...
  ] { class_ := "card", id := s!"comment-{c.id}" }

そのonClickは、コメントを削除するために必要なフロントエンドコードのすべてです。Datastar、ページ上の小さなスクリプトが、アイコンをクリックするとDELETEリクエストを送信します。その後、サーバーの応答でページを更新します。サーバーは、JSON APIが使用するのと同じ関数でその応答を構築します。ページはHTMLと1つのスクリプトだけなので、フロントエンドのビルドステップはありません。サーバーでは、Carlo Hamalainenと私がメンテナンスしているDatastarの公式Lean SDKであるdatastar-leanを使用しています。

［画像: 記事ページ。本文はlean-markdownによってレンダリングされたMarkdownで、フォローボタンといいねボタンはDatastarを通じてインプレースで更新されます。］

図2. 記事ページ。本文はlean-markdownによってレンダリングされたMarkdownで、フォローボタンといいねボタンはDatastarを通じてインプレースで更新されます。

定理1の証明。 3つの部分を組み合わせ、結果に対して両方のテストスイートを実行します。それらはパスします2。∎

補足1（コストについて）。Leanバックエンドは1,033行になり、比較した4つの実装の中で最も短いです3。TypeScript版は1,267行、Go版は1,371行、C#版は2,396行です。使用した11のライブラリのうち10はPaul Butcherによるものです。Claude Codeと私は、そのうち6つに修正を提供しました4。

3 本番環境

ラップトップでテストに合格しても、アプリが実際のユーザーに提供できるとは限りません。そのため、2番目の質問は本番環境についてです。

質問2. 定理1の実装は実際のユーザーにサービスを提供できますか？

2つの問題があります。

補足2（若いスタック）。LeanのHTTPサーバーは、プロセスあたり毎秒数千リクエストが上限です。これは主にLeanのランタイムのバグによるものですが、そのバグはすでに修正されており、まだリリースされていません5。Leanは毎月新しいバージョンもリリースします。新しいバージョンはライブラリを壊すことがよくあります6。バージョンを固定している小さなサイトにとっては、どちらの問題も重要ではありません。

補足3（誰が書いたか）。このコードのほとんどは手書きではありませんでした。Claude Codeが私の指示でアプリを書きました。ほとんどのライブラリも同様の方法で書かれました。すべて数ヶ月前のもので、ほとんどはコントリビューターが1人か2人しかいません7。このように速く書かれたコードは、まだ多くの読者やユーザーがいません。そのため、実際の使用で見つかるような種類のバグは、まだ残っている可能性があります。

最も信頼できる部分は、型と定理です。なぜなら、Leanがそれらをチェックするからです。それらは、誰が、あるいは何がコードを書いたかに関わらず有効です。ライブラリがAIエージェントに与える指示は、この方向性を促します。それらは「主張が許容する最も強力な形式：プロパティに対する証明された定理…例と期待される結果」を求めます。また、欠けている証明のプレースホルダーとしてsorryの使用を禁止しています。いくつかのライブラリには実際の証明が含まれています。定理でカバーされていないコードは、テストと同じくらいしか信頼できません。これはCライブラリへのバインディングではさらに顕著であり、LeanはCコードをまったくチェックできません。

それでも、証明された部分を読む必要があります。Leanは各証明が正しいことをチェックしますが、定理が実際に必要なことを述べているかどうかをチェックすることはできません。証明を求められたエージェントは、重要でないことを証明することがよくあります。Dan LuuがコーディングエージェントにZstd圧縮を実装させ、Lean 4を使用するように指示したとき、それらはバグが発生しやすいコードを見逃して、ほとんどが算術的事実を証明しました。それらの証明はコードをより正しくしませんでした8。したがって、定理と証明を含め、すべてを読む必要があります。それがあなたに必要なことを行っているか確認し、そうでない場合は修正してください。自分でチェックしていない部分を信頼しないでください。

claimcheckのようなツールは、その読書を助けることができます。それは、定理が何を意味するのかを知らずに、各定理をプレーンな英語で言い換えるAIモデルを持っています。2番目のステップは、その言い換えを元の意図と比較します9。それは有用なチェックですが、読書に取って代わるものではありません。

質問2への部分的な回答。では、アプリは実際のユーザーにサービスを提供できるのでしょうか？はい、ただし3つの条件が満たされている限りです：（H1）トラフィックが控えめであること、（H2）ツールチェーンを固定すること、（H3）誰かが実際にコードを読むこと。トラフィックが控えめな間は、サーバーの制限は問題になりません。状態をリクエスト間で保持しないため、より多くの負荷に対応するためにアプリのコピーをいくつか実行することもできます。固定されたツールチェーンは、アップグレードを選択するまで新しいLeanリリースが何も壊せないことを意味します。アプリは約1,600行しかないため、コードを読むことは最も重要な部分で可能です。実際のユーザーが見る前に、ハンドラー、SQL、Cバインディングを注意深く読む必要があります。

4 正しさ

特にAIがコードの大部分を書く場合、構築による正しさ（correctness by construction）を目指すべきだと私は考えています。それは、まずプログラムが正確に何をすべきかを形式言語で書き出すことを意味します。次に、コードはその記述から、それぞれが正しいと証明されたステップで導出されます。

今日、ほとんどの人は代わりにテストに依存するか、エージェントに仕様を与えてそれに従うことを期待します。テストは、誰かが書くことを考えたケースしかチェックしません。Dan Luuの実験は、エージェントが、使用するテクニックを指示されても、貧弱なテストを書くことも示しています。仕様だけでは、コードが実際にそれに従っていることを示すことはできません。構築による正しさは、Leanが仕様からコードへの各ステップをチェックするため、このギャップを埋めます。AIが与える速度を維持しながら、高品質なコードを出荷するための唯一の信頼できる方法です。

したがって、最後の質問は、このアプリが構築によって正しいことができるかどうかです。ここに正確な定義があります。

定義2. プログラムが構築によって正しいとは、形式仕様から、正しさを維持することが証明されたステップで導出されることである10。

質問3. Leanで構築によって正しいRealWorld実装は存在しますか？

定義2には、形式仕様とそれからの段階的な導出という2つの部分があります。それぞれをチェックしましょう。

仕様。 RealWorldには形式仕様がありますか？一部あります。その契約は、OpenAPIファイルとテストスイートです。OpenAPIファイルは、エンドポイントの数、それらが取るフィールド、返されるステータスコードなどの形状について正確です。エンドポイントが実際に行うことは、英語でしか説明されていません。テストは、チェックする特定のケースについてはそれを固定しますが、それ以外ではありません。したがって、RealWorldは型については形式的であり、動作については非形式的です。

導出。 アプリはその仕様から導出されましたか？いいえ。それは意図的な選択でした。RealWorldは型についてのみ形式的であるため、アプリの動作を導出するのに十分正確なものはありません。仕様が現状のままであれば、完全な構築による正しさは不可能でした。そのため、まずアプリを書き、後でテストしました。これは定義2が求めることの逆です。代わりに、検証するいくつかの重要なプロパティを選択しました。それらのうち3つは、コードがコンパイルされるという事実だけで保証されます。それらは次のとおりです。

命題1. ハンドラーの型がルートと一致しない場合、コードはコンパイルされません。

証明。 lean-routingは、各ハンドラーの型をそのルートから導出します。OpenAPIファイルは、コメントのIDは整数であると述べています。ルートテーブルもNatと述べています。したがって、IDをStringとして取るハンドラーはコンパイルされません。

error: Application type mismatch: The argument
  deleteComment env
has type
  String → String → Api.Handler
but is expected to have type
  HandlerType Api.patterns.comment Result

このエラーは、アプリが実行される前にコンパイル時に表示されます。∎

ExpressやGoのすべてのハンドラーは、ID自体を解析します。Rustのaxumでの不一致は、リクエストが来たときにのみ表示されます。ここに1つの弱い点が残っています。ルートテーブルをOpenAPIファイルから手動でコピーしました。ファイルを自動的に生成することで、このギャップを埋めることができます。

スラッグは、小規模ながら定義2を示しています。スラッグは、how-to-train-your-dragonのような、タイトルをURLフレンドリーにしたバージョンです。RealWorldはスラッグがどのように見えるべきかについて何も述べていないため、まずLeanのValidという型として仕様を記述しました。単一の小文字または数字は有効なスラッグです。有効なスラッグの前に文字または数字を付けるか、文字または数字の後にハイフンを付けることで、有効なスラッグを成長させることができます。それ以外は無効です。これにより、空のスラッグ、末尾のハイフン、二重ハイフンが除外されます。Slugは、それがこれらのルールに従っているという証明と一緒にバンドルされた文字列です。

inductive Valid : List Char → Prop where
  | single {c} : isSlugChar c → Valid [c]
  | cons {c rest} : isSlugChar c → Valid rest → Valid (c :: rest)
  | hyphen {c rest} : isSlugChar c → Valid rest → Valid (c :: '-' :: rest)

structure Slug where
  toString : String
  valid : Valid toString.toList

命題2. アプリが保存するすべてのスラッグは正しくフォーマットされています。

証明。 スラッグを保存する関数はSlugのみを受け入れるため、保存されるすべてのスラッグはその証明を運びます。それらの証明のほとんどは、タイトルをスラッグに変換するofTitleから来ています。それは、結果がすべての可能なタイトルに対して有効であるという証明を伴うため、コンパイルされるだけです11。∎

ofTitleは次のとおりです。これは、タイトルの文字と数字を保持し、それらを小文字に変換し、その間のすべてを単一のハイフンに変換するヘルパーcharsを呼び出します。その後、ofTitleはその文字列とそれが有効であるという証明を返します。証明はbyの後の部分です。

def ofTitle (title : String) : Slug :=
  match h : chars title.toList false false with
  | [] => ⟨"article", ...⟩   -- a title with no letters or digits
  | c :: cs =>
    ⟨String.ofList (c :: cs), by
      rw [String.toList_ofList, ← h]
      exact (chars_valid title.toList false).resolve_left (by rw [h]; exact List.cons_ne_nil _ _)
    ⟩

その証明はcharsに関する補題に依存しています。それは、任意のタイトルに対して、charsが何も返さないか、または有効なスラッグを返すことを述べています。補題は、タイトルの文字に対する帰納法によって証明されます。

theorem chars_valid (cs : List Char) (pending : Bool) :
    chars cs false pending = [] ∨ Valid (chars cs false pending) := by
  induction cs generalizing pending with
  | nil => exact Or.inl rfl
  | cons c cs ih => ...

合計で、これは10行のコードに対して約40行の証明です。プロパティベースのテストは、数千のランダムなタイトルをチェックします。証明は、誰もまだ書いていないタイトルを含め、すべてのタイトルをカバーします。

命題3. コードがNode.unsafeRawを呼び出さない限り、ユーザーが入力したものはすべてページに表示される前にエスケープされます。

証明。 lean-htmlでページ要素を直接構築することはできません。lean-html独自の関数のみが可能です。Node.unsafeRawを除くすべてが、そのテキストをescapeを通して実行します。lean-htmlは、escapeが決してその出力に<、>、または"を残さないことを証明しています。

def escapeChar (c : Char) : String :=
  match c with
  | '&' => "&amp;"
  | '<' => "&lt;"
  | '>' => "&gt;"
  | '"' => "&quot;"
  | c    => String.singleton c

theorem escape_safe (s : String) : 
    ∀ c ∈ (escape s).toList, c ≠ '<' ∧ c ≠ '>' ∧ c ≠ '"' := ...

平易な言葉で言えば、任意の文字列のエスケープされたバージョンには、<、>、または"は含まれません。∎

RealWorldのウェブサイトテストは、クロスサイトスクリプティングをチェックします。それらはAPIを通じて悪意のあるテキストを注入し、ページがそれをプレーンテキストとして表示することを確認します。このアプリのようにAPIとページの両方を提供するアプリの場合、スイートはそのテストをスキップします。したがって、ここでは証明が唯一のチェックです。Reactも同様にテキストをエスケープしますが、そこではテストのみがエスケープが正しいことをチェックします。

したがって、このアプリは構築によって正しいわけではありません。LeanでRealWorldアプリが（質問3）構築によって正しいことができるかどうかは、まだ未解決です。それに答えるには、まずRealWorldの動作をLeanで記述することから始める必要があります。アプリをそこから導出するには、SQLのモデル、および下位のCライブラリとStd.Httpに関する証明も必要になります。今のところ、スラッグは、この方法が最後まで実行された唯一の部分です。

アプリと両方のテストスイートを実行するための指示は、リポジトリにあります。

謝辞。 このプロジェクトを可能にしてくれたPaul Butcher氏、およびdatastar-leanのCarlo Hamalainen氏に感謝します。