bendlang/bend

Bend – 組み込み証明を備えた高速な並列言語

概要 – Bendは、高性能コンパイラ（CPUでCレベル、GPUでCUDAレベルの速度を目指す）と証明支援系スタイルの型システムを組み合わせたオープンソースのプログラミング言語です。この言語では、LAWS.bendというファイルに laws（形式仕様）を記述できます。コンパイラはコード変更に対して数学的な証明を要求し、それらの仕様が決して破られないことを保証します。AIが生成したコードを、人間が一行ずつ読むことなく信頼できるようにするための手段として位置付けられています。

コアコンセプト

• 高速実行 – 強力な静的型、純粋性、線形性により、コンパイラは手書きと同等の速度で動作し、数千のGPUコアにスケールするネイティブなC、Metal、CUDA、またはJavaScriptコードを生成します。
• 高速検証 – 同じコンパイラが1秒以内に証明をチェックします。これはIsabelle、Agda、Lean、Coqといった従来の証明支援系よりもはるかに高速です。
• 暗黙的な並列処理 – 明示的なスレッドやロックは不要です。ランタイムが自動的に純粋な計算をすべての利用可能なCPU/GPUコアに分割し、結果を結合します。
• 法則駆動開発 – LAWS.bendファイルは不変条件（例：「すべての残高の合計はゼロでなければならない」）をエンコードします。コードが編集されると、コンパイラは不変条件が維持されていることの証明を要求し、それに違反するAI生成の変更をブロックします。

典型的なワークフロー

1. LAWS.bendに1つ以上の法則を記述する。
2. LLM（または人間）にコードの実装や修正を依頼する。
3. bend PROOF.bendを実行する。コンパイラが法則に基づいて証明をチェックする。
4. 証明が成功すればコードは高速な実行ファイルにコンパイルされ、失敗すれば変更は拒否される。

構文例（依存型を持つPython風の構文）

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    name : String <- IO.try(String, IO.get_env("USER"))
    IO.print("Hello, " ++ name)

法則とその証明：

law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def add_zero(x):
  match x:
    case 0n: {==}
    case 1n+xp:
      %add_zero(xp) : {1n+Nat.add(xp, 0n) == 1n+_ : Nat}
      {==}

リポジトリの主要コンポーネント

• bend2/ – コンパイラと標準ライブラリ (base.bend)。
• paper/ – 型理論 (BendTT) と並列ランタイム (BendRT) を説明する学術PDF。
• bench/ – パフォーマンスチャートに使用されるベンチマークプログラム。
• tools/bend-fmt-lsp – 構文のみの言語サーバー機能を提供するフォーマッタ/LSP。
• demos/ – それぞれ独自の LAWS.bend を持つ小さなサンプルアプリケーション。

インストール

curl -fsSL https://bend-lang.com/install.sh | sh

このスクリプトは bend コマンドラインツールをインストールし、コンパイル、bend guide の実行、コードのフォーマットなどに使用できます。

現在の制限事項（READMEに記載）

• コードが冗長：すべてに注釈が必要で、型推論がない。
• 型クラス、トレイト、コンパイル時テンプレート以外のマクロがない。
• 証明探索/タクティクスがない。証明は手動で記述する必要がある。
• アフィン値のため、クロージャや配列を自由に共有できない。
• 標準ライブラリが限定的（TLS、HTTP、JSON、正規表現などがない）。
• 単一ファイルプログラムのみ。インクリメンタルビルドがない。
• GPUサポートはプログラムごとに1デバイスに限定。マルチマシン実行がない。
• Windowsはファーストクラスのターゲットではない（WSLは動作する）。JavaScriptターゲットはシングルスレッドで動作する。
• ツールが最小限：フォーマッタLSPのみで、デバッガー、プロファイラー、REPL、高度な診断機能がない。
• コンパイラ自体が大部分AIによって生成されており、完全な監査を受けていない。

コミュニティとリソース

• ウェブサイト：https://bend-lang.com
• Discord、Twitter/X、Reddit、GitHub issues（サポートと議論用）。
• 完全な言語ガイド (GUIDE.md)、正式なLeanモデル (bend.lean)、学術論文（より深い理解のため）。

結論 – Bendは、AIシステムによって生成される検証可能で高性能なコードという新たなニーズに応える、実用的かつ積極的にメンテナンスされている言語プロジェクトです。まだ初期段階であり、多くの便利な機能が欠けていますが、高速実行 と 高速な証明チェックという核心的な約束は、システムプログラミング、形式検証、AI支援開発の交差点における注目すべき実験と言えます。