ハクソク

世界を動かす技術を、日本語で。

Bend 2とバイブコーディングトラップ

2026年9月18日原文(blog.liampwll.com)

概要

  • Bend の設計を例に、「vibe-coding」の落とし穴を指摘
  • Bend はAI時代向けの新言語だが、既存の形式手法を無視
  • SPARK との比較で、現代的な形式検証とのギャップを解説
  • 事前調査の重要性と vibe-coding のリスクを強調
  • LLMの提案に頼りすぎる問題点を明確化

Bend言語設計におけるvibe-codingの罠

  • Bend はAI時代のための新言語として注目される高プロファイル事例
  • 人間が「法則」を記述し、AIが実装や証明を書き、コンパイラが証明の正当性を検証する設計思想
  • デモプログラムでは、プレイヤーが旗に触れたり勝利したりできないことを示すだけで 58行 のコードが必要
  • LLMによる証明生成はさらに 442行 と非常に冗長
  • 形式検証という分野の知見が Bend の設計やドキュメントにまったく登場しない問題
    • 形式検証（Formal Verification）というキーワードすら Bend のWebページやコードベースに見当たらない

SPARKによる同一要件の実装比較

  • SPARK はオープンソースの形式検証対応言語
  • Bendのデモと同じ要件（プレイヤーが勝利できない）を 簡潔なコード で実装可能
    • 法則と証明が一体化し、冗長な証明コード不要
    • GNATprove を使えば「全てのチェックが証明された」と即座に確認
  • 形式検証分野の標準的アプローチが既に存在し、 Bend はそれを無視している

vibe-codingのリスクと教訓

  • vibe-codingは「雰囲気」で設計や実装が進み、 本質的な調査や既存知見の活用を怠る 傾向
  • その結果、 時代遅れ や 非効率 な設計が生まれやすい
  • LLMに「証明付きプログラム言語を作って」と頼むと、既存技術を無視した冗長な解決策を提案しがち
    • LLMは「既に存在する標準的アプローチ」の利用を自発的に勧めない
  • 事前に分野調査を行い、 既存技術や標準手法に目を通す ことの重要性
  • Bendの例は、 vibe-coding の危険性や、LLMや新技術を使う際の落とし穴を示す好例

Hackerたちの意見

このプロジェクトに関する元の議論はめちゃくちゃ変だよね。著者が何かのセレブみたいに持ち上げられてて、ランダムなアカウントが彼を擁護してるけど、内容についての議論はほとんどない。リリースされたデモすらちゃんと動いてないし。

└

元の会話は最初からすごく臭かった。GitHubのページには2万スターもついてるけど、その歴史は失われてるし。

└

それがどんな領域か、私たちは知ってるよね。

└

元の議論で厳しい批評を投稿したんだけど、プロジェクトを批判しつつも礼儀正しくしようとしたんだ。ちょっと短気だったかもしれないし、今なら混乱を避けるためにいくつかの表現を変えるかもしれないけど、決して失礼だったとは思わない。著者の個人的な資格に焦点を当てた感情的な反応がいくつか返ってきたけど、それはすごく場違いに感じたし、私が言ったことに対して実質的に関わってこなかった。ほんとに変だった。昨日まで知らなかった著者が、実はすごくいい人みたい。彼はかなり反応が良くて、普通で、私のフィードバックにもちゃんと応じてくれたから、彼の代わりに怒ってるランダムなアカウントがいるのがさらに不気味だった。

└

アプローチ自体は、100以上の法律があるようなドメイン中心の記録システムなど、非自明なシステムには実用的ではないと思った。とはいえ、数年後にそのシステムがまだ準拠しているか、正しい原則に従っているかを確認するためのサイドパラレルスレッドとして試してみることはできるかもしれない。どのように採用されるかを見るまで待ちたいな。Bend 2の初期レビューを知っている人いる？

└

（著者です）何がうまくいってないの？このスレッド全体に対する返答も書いたよ： https://news.ycombinator.com/item?id=49753898

└

HNは、雰囲気コーディングのスラップをフロントページに載せて、信頼性を与えるためにゲームされ続けてるね。数週間前に「Wyzer」っていう言語プロジェクトがあったけど、完全に生成されたもので、ほとんど意味不明だった（ドキュメントが主張してるような高尚なことは全然できてなかった）。コメントはどれも絶賛ばかりで、批判には厳しく反応してて、ちょっと奇妙だった。

└

なんか、プログラミング界にLLMを使ったソカル・ホックスを仕掛けようとしてる人がいる匂いがする。

Bendの著者は、これが形式検証の分野での現在の標準だってことを完全に見落としてるみたいだね。この分野が存在することすら知らないかもしれない。代わりに、冗長な仕様やさらに冗長な証明を必要とするシステムを考え出してる。全体の言語やコンパイラをバイブコーディングする前に少しリサーチすれば、結果が大きく改善されたはずだよ。著者が何を求めるべきかを知ってたらね。 > この例はBendを超えて重要だよ。バイブコーディングは、研究をせずにすぐに結果を得られるから、ひどく壊れたデザインや数十年遅れのものを実装するのが簡単すぎる。もしLLMに、基本原則から証明を構築して関数が形式的に正しいことを証明できる言語を求めたら、喜んでそうするだろうけど、コンピュータがすでに複雑な証明をLLMなしで構築できることや、99%の作業を省けることを提案することは決してない。あなたが構築しているものは、すでにほとんど存在している作業として利用できることも教えてくれない。--- だから、何か重要なものを作るためのLLMリクエストは「まずは先行研究を行う」から始めるべきなんだ。もちろん、いつかすべてが収束する（もし私たちが成果物をオープンソースで共有すれば）ときが来て、しっかりした標準パターンやライブラリができるかもしれない。その時、同じ小さな基本的なものを再構築するために、世界中で何兆ものトークンを無駄にする必要はなくなる。もし私たちが共有すれば、もちろんLLMプロバイダーには収入が減るという経済的なデメリットがあるし、今や彼らは私たちの集合的な入力や考え、人間の「思考の痕跡」をメタデータで集めて、それを新しい「イノベーション」として再パッケージしてIPOや株価を膨らませることもできなくなる。

└

それとも、LLMにタスクを任せる前に考えるべきことがもっとあるかもしれないっていうフラグかもね。

└

「まずは先行研究を行う」。これは「間違いを犯さないように」と同じくらい効果的だね。これはあなたを喜ばせようとしていて、常にあなたを喜ばせる方法は元の核心的なリクエストを満たすことだと決めてる。注意事項や最初のステップは、常に「この人はXをやりたいから、私はXをする」っていう最終目標に対して二次的なものになる。私が一貫して役立つと感じた唯一の最初のステップは、技術的なトラブルシューティングをする時に「答える前にXのドキュメントを見てみて」って言うことなんだ。そうすればマニュアルとかを検索してくれる。推測を避けるのに役立つよ。でも、それでも完全に信頼できるわけじゃない。サイドバー：これが現在のLLMの核心的な問題の一つなんだ。彼らに特定の方法で振る舞わせるためにずっと議論してる感じで、彼らが言われた通りにやってるかどうかも常に明確じゃない。さらに、会話が長引くほど、誤解したり無視したりする可能性が高くなって、文脈の長さによる混乱に陥る。

└

人間はLLMに生のインターネット検索をさせないよ。

Hacker Newsで議論の続きを見る