Bend言語リリース – AIによる誤りを防ぐ証明付き、高速なCPU/GPUコンパイル

Bendが謳うメリット

Bendは主に3つの利点を提供します：

ネイティブ速度の実行 – コンパイルされたバイナリは、シングルCPUコアでC言語に近い速度で動作し、16コアやGPUを使用すると最大124倍高速になります。
即時の証明チェック – 型チェッカーが証明チェッカーとして機能し、ユーザー定義の「法則（laws）」を1秒未満で検証します。これは、同等のコードベースにおけるIsabelle、Agda、Lean、Coqよりもはるかに高速です。
自動並列化 – 明示的なスレッド処理やカーネルコードは不要です。ランタイムが利用可能なすべてのCPUコアやGPUコアに作業を分散し、結果を自動的に結合します。

これらの主張は、Bendのウェブサイト上のベンチマーク（Game of Life、pow2など）や、「勝利は不可能である」という法則を使用してAIが生成したバグをブロックする短いデモで実証されています。

高速なコンパイルと実行

Bendはネイティブマシンコードにコンパイルされます。Apple M4 Maxプロセッサでの報告された実行時間は以下の通りです：

1コア: 7.80秒 (C言語の6.78秒とほぼ同等)
16コア: 0.65秒 (約12倍の高速化)
GPU: 0.06秒 (約124倍の高速化)

サイトでは、これらの数値をTypeScript（18.8秒）、Lean（13.8秒）、C言語（6.78秒）と比較しています。GPUベンチマークでは、同じバイナリを4,096個のGPUコアで実行しており、ユーザーがカーネルを書かなくてもランタイムが大規模な並列処理を活用できる能力を示しています。

AIのミスを防ぐ証明ベースの「法則（laws）」

Bendは、開発者が決して破られてはならない不変条件を宣言するファイル LAWS.bend を導入しています。AIエージェント（Claudeなど）がコードを生成すると、コンパイラは宣言された法則に対して生成された PROOF.bend をチェックします。法則が破られる場合、コンパイルは失敗し、AIは法則が守られているという証明を作成できるまで再試行しなければなりません。

法則の例（勝利シーケンスが存在しないこと）：

# LAW: no move sequence leads to victory.
law you_cant_win:
  for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False{}

対応する証明を PROOF.bend で提供する必要があります：

# PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
  # ... AI‑generated proof

システムは法則を「型」として扱います。法則に違反するコードはコンパイル時に拒否されます。

並列ランタイム (BendRT)

BendRTは、純粋関数呼び出しを利用可能なコアに自動的に分散するランタイムです。この言語では、明示的なスレッド作成、ロック管理、CUDAカーネルの作成は不要です。作業は分割され、並列実行され、結果は透過的に結合されます。デモでは、pow2.bend プログラムが単一のコマンドで4,096個のGPUコア上で実行される様子が示されています。

Hacker Newsでのコミュニティの反応

賞賛と関心

ユーザーは、高速なネイティブコンパイルと、AI生成コードを対象とした形式検証を組み合わせた斬新なアプローチを評価しています。
スケジューリングや契約履行などの分野において、不変条件駆動開発の可能性を見出す声もあります。

懐疑的な意見と実用上の懸念

証明の労力: 必要な法則や証明を書くのは手間がかかるという指摘が複数あります。あるユーザーは、単純なカレンダーのcronジョブのために約60行の基本的な算術補題が必要だったと報告しています。
ツール不足: 既存のライブラリとの統合方法、証明のプロジェクト間での再利用性、法則が欠落または誤っている場合の対処法について疑問が投げかけられています。
リポジトリの透明性: GitHubリポジトリには最近のコミットが1つしかなく、コミット履歴が見当たらないため、プロジェクトの成熟度と信頼性に疑問が呈されています。
パフォーマンスの限界: BendのGPUパフォーマンスをFutharkのような専門言語と比較し、バランスの取れた再帰的なワークロードには適しているが、密な配列カーネルでは遅れる可能性があると指摘する観察者もいます。
強制力の保証: LLMが単に法則を無視することをどう防ぐのかという質問に対し、コンパイラが有効な証明を提供しない生成コードを拒否するため、AIは証明を作成するように誘導される必要があると回答されています。

注目すべき引用

「LAWS.bendは、証明によって裏打ちされたAGENTS.mdです。『ミスをしない』ことが型チェックされるようになりました。」 – Bendウェブサイト

「私が最も望んでいた法則は『2つの出力計画が重複しないこと』でした。私はそれを明示しませんでした。それにはcollapseの入力がソートされているという仮説が必要で……それが『原理的に証明可能』と『今日の午後までに証明可能』の間の正直な隔たりです。」 – svachalek

「2万スターで、1時間前のコミットが1つだけ？何頭のヤギが生贄に捧げられたんだ？」 – plastic041 (リポジトリの履歴に対する懸念を表明)

始め方

インストール（単一スクリプト）：

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

AGENTS.md にガイダンスを追加し、AIエージェントがガイドを実行し、法則を使用し、コミット前に証明チェッカーを呼び出すようにします。
重要な不変条件に対して法則を記述し、AIにコードと付随する証明を生成させます。
コンパイルされたバイナリをCPUまたはGPUで実行します。ランタイムが自動的に並列化します。

未解決の課題と今後の展望

証明のスケーラビリティ: すべての移動シーケンスを列挙することが不可能なほど巨大な状態空間を、Bendはどう扱うのか？
相互運用性: 既存のC/Rustライブラリを呼び出すためのFFIバインディングや、Bendコードをより大きなプロジェクトに埋め込む方法は提供されるのか？
ツールの成熟度: コミュニティは、信頼を築くために変更履歴、バージョン管理されたリリース、より明確なコミット履歴を求めています。
ベンチマーク: Bells ベンチマークスイートなどでの独立したパフォーマンス測定が、主張されている高速化の検証に役立つでしょう。

参考文献

ガイド: リポジトリ内の GUIDE.md (言語仕様の全容)。
BendTT論文: 言語の基礎となるアフィン依存型理論。
BendRT論文: CPUおよびGPU向けの並列ランタイムの解説。

Bendは非常に初期段階のプロジェクトです。バグや急速な反復が予想されます。貢献や問題報告はGitHubのissueトラッカーで歓迎されています。