bend

Bend 2は、ポストAGI時代に向けて設計された新しいプログラミング言語です。この時代では、人間が曖昧さのない言語を通じてAIシステムに意図を伝えます。その中核となる革新はLAWS.bendです。これは、開発者が不変条件（法則）を宣言し、AIがコード変更に対して数学的に証明を実行することを要求するメカニズムで、これらのルールに違反するバグのマージを数学的に不可能にします。 READMEに示されている主な機能は以下の通りです： **性能**: CPUではC言語レベル、GPUではCUDAレベルの速度を目標としています。ベンチマークでは、競争力のあるシングルコア性能と、数千コアにわたる大規模な並列スケーリングを示しています。コンパイラは、強い型、純粋性、線形性を最適化に活用します。 **証明チェック**: Isabelle、Agda、Lean、Coqよりも桁違いに高速な検証を主張し、複雑な証明を1秒未満でチェックします。 **暗黙の並列性**: スレッド、ロック、カーネルを書く必要はありません。分割統治関数は、利用可能なすべてのCPU/GPUコアに自動的に分散されます。例では、pow2(20)が4,096のGPUコアに分散される様子が示されています。 **AI協調ワークフロー**: AI支援開発向けに設計されています。開発者はLAWS.bendで法則（例：「残高の合計はゼロでなければならない」「プレイヤーは壁を通り抜けられない」）を書き、AIにコミット前に`bend PROOF.bend`の実行を要求します。コンパイラは証明を機械的に強制します。 **言語機能**: Pythonに似た構文と依存型を備えています。アフィン/線形型システム（値は共有不可）。終了する再帰が必要（@unsafeエスケープ付き）。C、Metal、CUDA、JavaScriptをターゲットにします。基本ライブラリは最小限で、エフェクトにはI/O、チャネル、TCP/UDP、ファイルアクセスが含まれます。 **現在の制限（明示的にリスト）**: 冗長な注釈、型クラス/トレイト/マクロなし、タクティクや証明探索なし、数値型が限定的（Nat、U32、F32のみ）、文字列が遅い（連結リスト）、HTTP/JSON/TLS/正規表現なし、プログラムごとに単一GPU、インクリメンタルコンパイルなし、ネイティブコンパイルが遅い、ツールが最小限（LSP、デバッガ、フォーマッタ、REPLなし）、コンパイラは主にAIが作成し未監査。 プロジェクトには、Leanでの形式化（bend.lean）、学術論文（BendTT型理論、BendRTランタイム）、成長中のデモコレクションが含まれます。コミュニティチャネル：Discord、Reddit、X/Twitter。提供された資料にはライセンスは記載されていません。