Bend：証明でAIのミスを封じる高速言語、C並みの速度でGPU並列も

歴史に関するかなりの量のコンテンツを消化した上での私の見解は以下の通りです：

- このBendは古いBendとは（名前だけを除いて）実質的に関係がない

- このBendはinteraction combinatorsとはほとんど関係がない

- このBendはQTTであり、アフィニティに変更を加えてGPU向けの優れたパフォーマンス特性を強制している

- 「comptimeでの高階」は素晴らしく、Andras Kovacsの2lttや依存型言語におけるステージングの研究を思い出させる

- このBendは「ADT上のバランスの取れた再帰計算」が得意で、それらを並列化できる可能性がある…しかし、密な矩形配列計算ではCUDAや例えばFutharkほど良くはないだろう

- パフォーマンスはスケジューラの改善が必要で、バランスの取れた作業を助ける可能性がある（n queensや記号回帰の数値を見る限り）？

不規則な構造に対する探索や合成（SupaGen）はどのように扱うつもりですか？

> ポストAGI経済では、人間は最終的にコードを書いたり読んだりしなくなるが、私たちの周りの世界を構築するAIに何をしてほしいかを伝えるための曖昧さのない方法が依然として必要だ。

> 法律を使えば、私たちの意図は自然言語よりもはるかに正確になる。

これはつまり、コードが今や「法律」になったというだけのことではないか。つまり、コードが今や仕様になったのだ。

そうだとすると、複雑なシステムの「法律」を書くことが、それを実装する昔ながらのコードを書くよりも簡単だと思う理由が何かあるのだろうか？

このプロジェクトのリポジトリは20Kスターでフォークは500しかなく、イシューも（クローズ済みを含めて）300未満だ。何かおかしい。

他のプログラミング言語と比較すると：

- Gleam: 22Kスター、1Kフォーク、3Kイシュー

- V: 38Kスター、2.3Kフォーク、11Kイシュー

- Ruby: 23Kスター、5.6フォーク、19Kイシュー

- Zig: 43Kスター、3Kフォーク、14Kイシュー

しかもたった4ヶ月で16Kスターを獲得している。https://www.star-history.com/?repos=bendlang%2Fbend

また、誰がこれを信頼するだろうか？1) 変更履歴 2) 古いバージョンをダウンロードする方法 3) コミット履歴 がないプログラミング言語なんて見たことがない。

なぜ作者がコミット履歴を削除するのが良い考えだと思ったのか理解できない。このプロジェクトを初めて見たと想像してほしい。20Kスターのリポジトリなのにコミットがなく、イシューやPRが不自然に少ない。正当なものには見えない。

---

学術的な手続きには詳しくないが、リポジトリにあるPDFで、Fableによって書かれ、レビューもないものは、私には適切な「論文」には思えない。

言わせてもらうと、2023年半ばからTaelinをこのプロジェクトで追ってきたが、この言語が最初にリリースされたときの反応は予想外だった。

化粧品が議論を左右すること、そしてHNのコメントが非常に軽蔑的または懐疑的な陣営と、前者の反応に不信感や怒りを感じている人々とに奇妙に分かれているのは興味深い。

代わりに私が期待していたのは、ユースケース、ベンチマーク、可能性、制限（git履歴に関するものではない）、そして将来の開発範囲についての議論がもっと多くなることだった。

クールなアイデアだ。バイブコーディングした小さな会議修正cronジョブを移植するのに使ってみたが、本質的にカレンダーの不変条件を満たそうとするものなので自然に合うと思えた。

基本的には成功したが、Claude（Opus 5）にはいくつか不満があった：

「Baseには算術法則が1つしかない、U32.add_comm。順序理論はない。PROOF.bendの163行のうち約60行はcmp_refl、and_false、and_comm、le_max_l、le_max_r、add_succ——存在すると思い込む事実だ。プロジェクトごとに一度書けば二度と書かないが、その分の予算を見込んでおく必要がある。」

「BaseのNat.maxは証明では使えない。Bool.pick(Nat, Nat.is_lt(a,b), b, a)であり、証明は計算値で場合分けできない。Nat.cmpと歩調を合わせて展開する構造的再帰のnat_maxを書いた。」

「最も欲しかった法則：『2つの出力プランが重ならない』。それは述べなかった。collapseの入力のソート性を仮説として必要とし、BaseのList.sortにはソート性の法則がない——だからそこに到達するにはまずマージソートが正しいことを証明しなければならない。これが『原理的に証明可能』と『今日の午後に証明可能』のギャップの正直な尺度だ。」

私はCSのマイナー程度なので証明に関しては素人だ。これが価値のあるフィードバックなのか、単にClaudeが何かを誤解しているのかはわからない。

サイトのデモでの主な経験は、ゲームに勝つことさえ必ずしもできないような簡単な機能を追加するように頼むと、100kトークン以上を「法則違反」のループに費やし、最終的に追加するかもしれないししないかもしれない、というものだった。壁を1行追加して2マス上にテレポートしても勝てないようにするだけで50万トークンを消費した後、APIキーがレート制限されてループが壊れた。

その上、解決策はパッチワークのように感じる。スペースバーで盤面を水平反転させてほしいと頼んだら、2本の旗竿を含めて盤面を完全に対称にしてしまった。ある時点で「法則を破らずには不可能だ」と言うか、実際の回避策を考えるべきだ。なぜなら、ゲームを作っているなら、突然2つのゴールがあるのは望ましくない動作だからだ。

> LAWS.bend

法則のアイデアは好きだが、結局彼らがやっているのは、取り組んでいる新機能に合わせて法則自体を修正してしまうことで、それでは意味がない。

つまり、一部の法則は凍結する必要がある。しかしすべての法則を凍結すると、何も追加・変更できなくなる。だから判断は依然として人間の側にあり、結局は肉袋がボトルネックに戻る。

エージェントが不合理なことをするたびに、こうした証明のようなチェックをCIに追加することで成功例を見たことがある。これはすべてのコードベースに含めるべきだと強く思う。

コードと証明を同じ場所に配置する https://code-contracts.cc/ もある。

> 人間は最終的にコードを書いたり読んだりしなくなる、

「FORTRANは事実上コーディングとデバッグを不要にするはずだ…」 -- FORTRANレポート、1954年

http://www.softwarepreservation.org/projects/FORTRAN/BackusE...

問題は、すべての法則をバイブコーディングしなければならず、その法則が間違っている可能性があることだ。