#形式手法

AIにコードを書かせる開発は、速い。けれど、その速さが「何を作るべきか」を見誤らせることがある。Liam Powell の記事は、Bend 2 という新しい言語を題材に、その危うさをかなり具体的に示している。面白いのは、彼が単に Bend をこき下ろして終わらせていない点だ。むしろ、AIで開発を進めるときに起きやすいズレを、別の言語と実例を使って説明している。 元記事が取り上げているのは、Bend 2 が「AI coding era」のための言語として打ち出されている、という話だ。人間は「laws」と呼ばれる仕様や制約を書く。AI は実装と proof を書く。コンパイラは、その proof が正しいかを検証する。見た目にはかなり野心的で、筆者も「そういうことをしたい人がいるのは分かる」と認めている。 ただし、彼の主張は Bend そのものの思想批判ではない。問題にしているのは、Bend が vibe-coding の罠にはまっているのではないか、という点だ。vibe-coding とは、十分に調べたり設計を詰めたりする前に、LLM を使って勢いよく実装を進めてしまうやり方を指している