#proof

AI にコードを書かせる流れが強まるほど、「速く動く」ことと「意図どおりに動く」ことの両立が難しくなる。Bend は、その矛盾を言語設計そのものから解こうとしているプロジェクトだ。作者は、自然言語で雑に指示しても AI が実装し、しかも proof で間違いを止められる世界を見据えている。まだ若い言語ではあるが、主張はかなり野心的で、今の AI 開発ブームに真正面から乗っている。 Bend は、AI のミスを proof で塞ぐことを売りにした新しい language だ。紹介文では「a fast language that blocks AI mistakes via proof」と掲げられ、あわせて C speed、CUDA parallelism、Lean proofs、Python syntax という特徴が並ぶ。つまり、書きやすさは Python に寄せつつ、実行速度は C に近く、しかも GPU も使える。そこに proof checker を組み合わせて、AI が書いたコードが守るべき規則を機械的に確認する、という構想になっている。 サイトの冒頭では、将来の post-A