HN 日本語サマリー

← 一覧へ戻る
プログラミング

Bend: AIのミスを防ぐ証明付き高速言語

Bend (bend-lang.com)

204 pointsby nicolas-siplis113 コメント

要約

Bendは、AIによるコーディングミスを証明によってブロックする新しいプログラミング言語です。ネイティブコードにコンパイルされ、C言語並みの速度とGPUでの大幅な高速化を実現し、並列処理も容易に行えます。LAWS.bendで定義された「法則」とPROOF.bendによる証明により、AIがバグを含むコードをコミットすることを数学的に不可能にします。

全文翻訳

インストール 1. curl -fsSL https://bend-lang.com/install.sh | sh 2. AGENTS.mdに以下を追加 Bendを使用する場合: - 学習するには `bend guide` を実行します - 重要なルールを維持するには `LAWS.bend` を使用します - コミット前に `bend PROOF.bend` を実行します - コードは可能な限り並列化します 3. バグがなく、高速なバイブコードアプリをお楽しみください! Bendは、証明によってAIのミスをブロックする高速言語です C言語並みの速度 · CUDA並列処理 · 厳密な証明 AGI後の経済では、人間は最終的にコードの作成と読書をやめることになりますが、私たちはAIが私たちの周りの世界を構築する際に、私たちが何をしたいのかを伝えるための曖昧さのない方法を依然として必要としています。法則があれば、私たちの意図は自然言語よりもはるかに正確になります。証明があれば、AIがプロンプトを正しく実装したことを検証できます。そして高速なコンパイラがそれを速度で実行します。それがBendであり、それ以外のものではありません。 1. Bendは高速に動作します。 Bendはネイティブコードにコンパイルされます。1コアでは、C言語とほぼ同等の速度で動作します。同じバイナリは16コアやGPUでも実行でき、1コアよりも最大100倍高速に動作します。 Apple M4 Max · 低い方が良い 2. Bendは高速にコンパイルされます。 Bendの型チェッカーは、LeanやRocqのような証明チェッカーでもあります。これらは中規模のコードベースでは数分かかることがあります。Bendは最大でも1秒しかかからないため、AIエージェントは変更ごとにチェックできます。 Apple M4 Max · 低い方が良い 3. Bendは並列化されています。 スレッド、ロック、カーネルの記述は不要です。作業を2つに分割すると、Bendは利用可能なすべてのコアに呼び出しを分散し、それらを結合します。次に、pow2が4,096のGPUコアで実行されるのを見てみましょう。 GPUで実行されるpow2.bend 4. Bendはミスをブロックします - 証明付きで 読んだことのないコードをどうやって信頼できますか?証明を要求することによってです。LAWS.bendは、法則を宣言する場所です。それ以降、どのAIも法則を破るようなコードを1行も出荷できなくなります。ゲームを保護する様子をご覧ください。 法則: 勝利は不可能 これまでのところ、うまくいっています!新機能: 「Claude、ボードをラップアラウンドさせて」 LAWS.bendなしの場合: 法則が破られました。AIのミス: マージされました。 LAWS.bendありの場合: 法則は維持されました。AIのミス: ブロックされました! LAWS.bendなしの場合、バグはそのまま公開されました。LAWS.bendありの場合、AIは法則が成り立つことを証明するまでリトライしなければなりませんでした。バグをマージすることは数学的に不可能であり、それは定理です。 LAWS.bend # 法則: いかなる移動シーケンスも勝利につながらない。 law you_cant_win: for moves: List<Move> # 任意の移動シーケンス board = replay(start(), moves) # 最初からリプレイされる is_won(board) == False{} # 決して勝利につながらない PROOF.bend # 証明: you_cant_win は成り立つ。 def Laws.you_cant_win(moves): # ... AIによって書かれる LAWS.bendは証明によって裏付けられたAGENTS.mdです。「ミスをしない」は型チェックされるようになりました。懐疑的ですか?ゲームを壊してみてください。 5. 開始方法。 5.1.インストール curl -fsSL https://bend-lang.com/install.sh | sh 5.2.エージェントにBendの使用を指示する AGENTS.mdに以下を追加します: Bendを使用する場合: - 学習するには `bend guide` を実行します - 重要なルールを維持するには `LAWS.bend` を使用します - コミット前に `bend PROOF.bend` を実行します - コードは可能な限り並列化します その後、単に次のように言います: 「Bendを使って!」 5.3.バグがなく、高速なバイブコードアプリをお楽しみください! ヒント: 壊れてはならないものには法則を作成させ、高速に実行したいものはすべて並列化させるように依頼してください。 Bendはまだ新しく、何か問題が発生した場合は、issueを開くように依頼してください。Bendはバックエンド、Linux、macOSで最適に動作します。お楽しみください!<3 6. 参考文献。 ガイド: GUIDE.md が言語全体です。bend guide はそれを表示します。 論文: BendTT、アフィン従属型理論、Bendのコア。 論文: BendRT、CPUおよびGPU向けの並列ランタイム、VM。 Bendはまだ進化中です。バグが発生する可能性がありますので、報告してください。