「デュアルプログラミングとエクソシストゲーム」において、自分で「俺のターン」とかのセリフを書いておきながら、duel(デュエル)のオチに気付かなかった僕、t_tradさんに突っこまれてしまったよ。相当にクヤシイ。
それはそうと、なんで悪魔が登場するのかっていうと、悪魔は超越的な能力を持っているので、理想的な状態の説明に使えるからです。悪魔のごとき行為は、人間には無理だし計算機にもできないでしょう。悪魔は理論上の存在です。
人間の実装者は、悪魔のように完璧ではないですし、悪魔のように意地悪でもないので、戦いというよりは対話と妥協が行われるのでしょうが、少しでも正確さを増すために呪文(形式的記述と検証系)を導入しては、って程度のことです。
エクソシスト=設計プログラマも、もちろん間違いを犯します。つまり、間違った呪文を唱えるってことですね。しかし、実装者が人間なら、「おまえの“意図”通りに実装した“つもり”なのに、なんでテストが通らないの?」といったフィードバックで修正できる可能性もあります。
結局、エクソシスト=設計プログラマも、悪魔=実装プログラマも人間である場合(同一人物であることも多い)、間違いは避けがたいです。ですが、信頼できる検証系で、相互のズレを検出することにより間違いを発見しやすくすることはできるでしょう。
こう書くと、たいした御利益はないようですが、あまりに御利益を期待しすぎるのがイケナイのだ、と僕は思います。論理式で仕様を書き下すのはホントに大変ですから、人間どおしの対話と妥協も必要なんですよ、実際には。
それと、簡単なデータ構造やアルゴリズムに対して、人間どおしがエクソシストゲーム=“デュエル”プログラミングをほんとにやってみるのは、教育的効果がけっこうあるような気もします。