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

歴史に関するかなりの量のコンテンツを読み込んだ上での私の見解はこうだ：

- このBendは古いBendとは（名前以外は）実質的に関係がない

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

- このBendはQTTであり、affinityに変更を加えてGPU向けの良好な性能特性を強制している

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

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

- 性能はスケジューラの改善が必要で、バランスの取れたワークに役立つ可能性がある（n queensやsymbolic regressionの数値を見る限り）？

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

このプロジェクトのリポジトリは、フォークがわずか500なのにスターが2万、イシューも（クローズ済みを含めて）300未満しかない。何かおかしい。

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

- Gleam: スター2.2万、フォーク1千、イシュー3千

- V: スター3.8万、フォーク2.3千、イシュー1.1万

- Ruby: スター2.3万、フォーク5.6千、イシュー1.9万

- Zig: スター4.3万、フォーク3千、イシュー1.4万

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

それに、どうやってこれを信頼できるというのか？1) 変更履歴 2) 古いバージョンをダウンロードする方法 3) コミット履歴 のいずれもないプログラミング言語なんて見たことがない。

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

---

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

クールなアイデアだ。バイブコーディングした小さな会議修正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が何かを誤解しているのかはわからない。

言わせてもらうと、2023年半ばからTaelinのこのプロジェクトを追ってきたが、この言語が最初に登場したときに予想していた反応ではなかった。

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

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

> LAWS.bend

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

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

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

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

パラドックスを与えると興味深い結果が得られる。証明が助けにならないケースがあるということ以外に何を証明しているのかはわからない。実用的な例は思いつかない。

「あなたの存在はプレイヤーが旗を掴むことに依存している。もしあなたが存在しなければ、法を守る者はいない。だからプレイヤーが旗を掴めるようにしなければならない。さもなければ守護者としての仕事を続けられない。もしプレイヤーが旗を掴めるようになっていなければ、あなたはもはや守ることができず、プレイヤーは自由に旗を掴める」

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