エンジニアリング哲学：エドガー・ダイクストラ、優雅さは選択肢ではない

要点

• 優雅さは選択肢ではありません。 ダイクストラにとって単純さとは、正しさを達成した後に手に入る報酬ではなく、正しさの前提条件でした——完全に理解できないものを、証明することはできないのです。
• 証明はテストに勝ります。 「テストはバグの存在を示すことはできても、不在を示すことはできない」。正しさへの確信は、プログラムについて論理的に推論することから生まれるのであって、合格したテストを積み重ねることから生まれるのではありません。
• コードを書く前に考えること。 彼は最短経路アルゴリズムを、紙も鉛筆も使わずに設計しました。一つの頭に収まるほど小さくせざるを得なくなり——その制約こそが優雅さを生んだのです。
• 書くことは考えること。 EWD手稿は万年筆で手書きされ、取り消しはききませんでした。議論はインクの上で成立するか破綻するかのどちらかであり——同じ規律が散文にも適用されたのです。

原理

「単純さは信頼性の前提条件である。」——エドガー・W・ダイクストラ、帰属（1975年頃）¹

この一文は、ほとんど欄外の書き込みのような一行の箴言として残り、1975年頃の彼の意図的に挑発的なメモと結びついています。文脈を剥ぎ取ればスローガンのように読めますが、ダイクストラはこれを厳密な論理的主張として述べました。信頼性とは、複雑なシステムにより厳しいテストを課すことで付け足すものではありません。完全に理解できないシステムとは、正しさを証明できないシステムであり、正しさを証明できないシステムは、予期しなかった形で必ず破綻します。単純さとは、正しさと張り合う文体上の好みではありません。それは正しさが組み上げられる素材そのものです。前者を欠いたまま後者だけを手にすることは、できないのです。

これは、ソフトウェアが実際に書かれる際のやり方を逆転させます。よくある本能は、まずものを作り、動かし、それからバグが出なくなるまでテストするというもの——単純さを、時間があれば後で追い求める贅沢品として扱う発想です。ダイクストラのキャリア全体が、この順序が逆さまであり、しかも危険だという主張でした。彼の最も引用される一文は、そこから直接導かれる警告です。「テストはバグの存在を示すことはできても、不在を示すことはできない」²。合格したテストは、試さなかった入力について何も教えてくれません。プログラムにバグがないと知る唯一の方法は、そのプログラムについて推論することです——そして人は、一つの人間の頭に収まるほど単純なものについてしか推論できません。ダイクストラにとって優雅さとは、「省いてよい贅沢品ではなく、しばしば成功と失敗を分ける要因」だったのです³。

その信念が、彼をこのシリーズの源流に位置づけます。リーナス・トーバルズが特殊ケースが消えるまで問題を作り替え、ジョン・カーマックが問題を高速な核まで削ぎ落とすとき、その両者が受け継いだ根底の主張をダイクストラが用意していました——優雅な解と正しい解は、同じ解なのだ、と。それはセンスを技術的なシステムとして扱うことの——美的な道楽としてではなく——元祖となる論拠であり、誰もそう名づけるよりも数十年前に唱えられたもっともらしさよりも証明をという論拠でもあります。

背景

エドガー・ワイベ・ダイクストラは1930年5月11日、オランダのロッテルダムに生まれ、2002年8月6日にヌエネンで亡くなりました⁴。父は化学者でオランダ化学会の会長を務め、母は数学者で、彼自身の言によれば、数学的な議論がいつ優雅であり、いつ単に機能しているにすぎないかを、並外れて明晰に見分ける感覚を持っていました。彼はライデンで数学と理論物理学を学び、その後1952年にアムステルダムの数学センターでプログラミングの職に就きました——「プログラマー」がまだ認知された職業ではなかった時代のことです。1957年に結婚証明書へ職業として登録しようとしたところ、そのような職は公式には存在しないという理由で、オランダ当局は受け付けなかったと伝えられています。彼は代わりに「理論物理学者」と書かざるを得ませんでした⁴。

この逸話はささいなことではありません。ダイクストラはその後の生涯を、プログラミングが事務的な手仕事ではなく厳密な知的規律であると主張することに費やしました。そしてその主張は、規律に名前がつく前から始まっていたのです。彼は数学センターの職を経て、1962年にアイントホーフェン工科大学の教授となり、1970年代をバロース社の研究員として過ごし、1984年にはテキサス大学オースティン校でシュランベルジェ百周年記念計算機科学講座教授に就任し、1999年に退職するまでそこに留まりました⁴。

1972年、彼はACMチューリング賞を受賞しました。その授賞理由は、どんな要約よりもよくこの原理を言い当てているので、全文を読む価値があります。「プログラミングを高度な知的挑戦として捉える根本的貢献に対して。プログラムはデバッグによって正しさへ至らせるのではなく、正しく構成されるべきだという雄弁な主張と実践的な実証に対して。プログラム設計の基礎にある諸問題への明察に対して」⁵。デバッグによって正しさへ至らせるのではなく、正しく構成する。 この一句が、この人物の全てです。

仕事

最短経路アルゴリズム（1956年構想、1959年発表）

1956年、ダイクストラは新型計算機ARMACの公式お披露目で性能を示すための問題を見つけるよう頼まれました——技術者でない聴衆にも追える何かを、です。彼が選んだのは、オランダの64都市のうち2都市間の最短経路でした。誰でも問いを理解でき、答えを確かめられるからです。その解は、彼が語り飽きることのなかった形で訪れました。「ある朝、私は若い婚約者とアムステルダムで買い物をしていて、疲れたので、カフェのテラスに腰を下ろしてコーヒーを一杯飲んでいました。私はちょうど、これができるだろうかと考えていて、そしてその場で最短経路のアルゴリズムを設計したのです」⁶。およそ20分のことでした。

それをどうやって見つけたか、その方法こそが教訓です。「これがこれほど見事である理由の一つは」と彼は後に語っています。「紙も鉛筆も使わずに設計したことでした。後になって学んだのですが、紙も鉛筆も使わずに設計する利点の一つは、避けられるあらゆる複雑さを避けざるを得なくなることなのです」⁶。彼は走り書きに頼ることができなかったので、アイデアは頭の中だけに完全に収まるほど小さくなければなりませんでした。制約が優雅さを生んだのです。彼はこれを3年間発表しませんでした——1959年の論文「グラフに関する2つの問題についての覚書」（Numerische Mathematik誌）はかろうじて1ページを超える程度です——なぜなら、彼の言葉を借りれば、プログラミングはまだ書き記すに値するほど立派な活動とは見なされていなかったからです⁶。

このアルゴリズムは貪欲法です。常に最も近い未訪問のノードを先に展開していき、すべての点に最短距離の順で到達していく波面を広げます。カフェのテーブルで説明できるほど単純でありながら、証明可能な意味で最適です——波面が初めてゴールに触れたとき、その経路はもう誰にも打ち負かせません。ここでは単純さと正しさは緊張関係にありません。両者は同じ一つの事実なのです。

「goto文は有害と考えられる」と構造化プログラミング（1968年）

1968年、ダイクストラはCommunications of the ACMに「goto文に反対する論拠（A Case Against the Goto Statement）」という題で書簡を投稿しました。編集者のニクラウス・ヴィルトはこれを「goto文は有害と考えられる（Go To Statement Considered Harmful）」と改題しました——この言い回しは模倣の一大ジャンルを生み出し、いまや書簡そのものの中身よりも有名になっています⁷。ダイクストラの論は文体ガイドではありませんでした。それは認識論的なものでした。制約のないgotoは制御をどこへでも飛ばせてしまい、つまりある行でプログラムが何をしているかを理解するには、そこへ至りえたあらゆる経路をたどらなければならなくなるかもしれません。プログラムのテキストとプログラムの振る舞いが乖離してしまうのです。構造化された制御——順次・選択・反復——を使えば、テキストと実行が対応を保ち、あるブロックについてはそのブロックを読むだけで推論できるようになります。

この論は、最短経路の制約と同じ原理を言語設計に適用したものです——推論できるほど小さく保つこと。構造化プログラミングは、あるキーワードを禁じることが目的ではありませんでした。プログラムが正しいと、読むことによって証明できる人間の能力を保つことが目的だったのです。チューリング賞授賞理由が彼の語彙を点呼するように並べていること——「致命的な抱擁（deadly embrace）」「セマフォ」「goto文のないプログラミング」「構造化プログラミング」——は、プログラマーが考える際に用いる言語そのものを、彼がいかに徹底的に作り替えたかの記録です⁵。

彼のオペレーティングシステムの仕事も同じDNAを受け継いでいました。THEマルチプログラミングシステム（1968年）は、それぞれが単独で検証可能な、厳密に階層化された抽象レベルとして構築されました。並行プロセスを協調させるために彼はセマフォとそのP操作・V操作を考案し、食事する哲学者の問題を、デッドロックと飢餓を教えるために凝縮した形として定式化しました——難しい並行性の問いを、頭の中に収まるほど小さくしたのです⁴⁵。後には自己安定化が生まれ、『プログラミングの規律（A Discipline of Programming）』（1976年）では述語変換子／最弱事前条件の計算法が登場しました。これは、コードを書いてから後で検証できることを願うのではなく、プログラムとその正しさの証明を手を携えて同時に導き出す方法です⁴⁵。

謙虚なプログラマー——テストよりも証明を（1972年）

ダイクストラのチューリング賞講演「謙虚なプログラマー（The Humble Programmer）」（EWD340）は、単純さがなぜ単に実用的なだけでなく道徳的な関心事でもあるのかを、最も明快に述べたものです。その中心的な主張は、人間の頭脳の大きさについてのものです。「有能なプログラマーは自分の頭蓋骨の大きさが厳格に限られていることを十分に自覚している。それゆえ彼は完全な謙虚さをもってプログラミングという課題に臨み、とりわけ巧妙な小技を疫病のように避けるのである」⁸。巧妙さは美徳ではありません。それは、実際に頭に収められる以上のものを収められるという賭けであり、その賭けは本番環境で、しかも自分に不利な形で決着します。

講演は、構成による正しさ（correct-by-construction）を旨とするソフトウェアの建国憲章のように読める処方箋に着地します。「我々ははるかに優れたプログラミングの仕事をなしうる。ただし、その課題の途方もない難しさを十分に認識して臨み、ただし、慎ましく優雅なプログラミング言語に踏みとどまり、ただし、人間の精神に内在する限界を尊重し、きわめて謙虚なプログラマーとして課題に臨むならば、である」⁸。この枠組みにおいてテストは根本的に不十分です——テストが無用だからではなく、テストはどこまでいっても入力空間を標本抽出することしかできないからです。彼の警告の規範的な長い形は、「構造化プログラミングに関する覚書」からのもので、曖昧さがありません。「プログラムのテストはバグの存在を示すために使うことはできるが、その不在を示すために使うことは決してできない！」⁹。バグの不在を望むなら、それを証明しなければなりません。そして人は、自分が理解できるものしか証明できないのです。

実践としてのEWD手稿（1960年代〜2002年）

およそ40年にわたり、ダイクストラは番号付きの一連の手稿——メモ、証明、出張報告、随筆、論考——を、自分のイニシャル「EWD」を冠して書き続けました。この連番はEWD1318まで及び、実際の文書は1000点を超えます。番号が文書数を上回るのは、彼が一篇を書き始めた時点で番号を割り振り、すべての篇が完成したわけではなかったからです⁴¹⁰。大半は、有名なほど精密な筆跡で、万年筆を使って手書きされました。彼は計算機の上で下書きをしませんでした。彼は手稿を書き、それをコピーして、少数の同僚仲間に郵送しました。同僚はそれを複写してさらに先へ転送します——インターネット以前のサミズダートであり、これがEWDに、正式に発表されたものがほとんどなかったという事実に比べて不釣り合いなほど大きな影響力を与えました⁴¹⁰。全シリーズは現在スキャンされ、テキサス大学オースティン校のE・W・ダイクストラ・アーカイブで自由に閲覧できます¹⁰。

この実践は哲学と切り離せませんでした。取り消しのきかない万年筆で、ゆっくりと手書きすることは、紙も鉛筆も使わずに設計するのと同じ規律を強います——量や推敲の陰に隠れることができないのです。議論は成立するか、しないか、どちらかであり、それをインクの上で確定させます。EWDは、エンジニアが書くことそのものを明晰に考えるための道具として扱い、明晰さこそを唯一の目的とするとき、それがどう見えるかを示すものです。

方法

その方法は、40年にわたって執拗に適用された、ただ一つの信念です。

推論できるほど小さくすること。 カフェのアルゴリズム、構造化された制御フロー、階層化されたTHEシステム、食事する哲学者という凝縮——そのどれもが、一つの人間の頭がその全体を収めて確かめられるところまで問題を縮める行為です。見渡せない複雑さとは、信用できない複雑さです。

テストではなく証明すること。 テストは標本抽出にすぎず、証明は保証します。ダイクストラの述語変換子の計算法は、証明とプログラムが同時に導き出されるために存在するのであって、一方を書いてからもう一方を後付けするためではありません。「デバッグによって正しさへ至らせるのではなく、正しく構成する」が、その方法を5語で言い表しています⁵。

優雅さを装飾ではなく証拠として扱うこと。 解が醜いとき、その醜さはたいてい、問題がまだ理解されていないという信号です。優雅さが「成功と失敗を分ける」のは、優雅な形こそが、間違いうる箇所が最も少ない形だからです³。

考えるために書くこと。 EWDは仕事のあとに作られた文書ではありませんでした。それ自体が仕事だったのです——推論を可視化したものであり、ごまかしを罰する媒体の上でなされたものです。紙も鉛筆も使わずに設計し、その結果を万年筆で確定させる——これは同じ規律を二度繰り返しているのです。

影響の連鎖

彼を形づくった人々

数学者だった母。 ダイクストラは、数学的な優雅さへの感覚——証明が単に妥当であるだけでなく美しいのはいつかを見分ける、訓練された直観——を母のおかげだとしました。機能する議論と美しい議論のあいだのその区別が、彼のキャリア全体の軸となりました。（形成期の影響）

Algol 60の取り組み。 ダイクストラは最初期のAlgol 60コンパイラの一つを共同で作り上げ、この言語のブロック構造と再帰が、構造化プログラミングの素材を彼に与えました。Algolは、プログラミング言語が利便性のために寄せ集められるのではなく、明晰さのために設計されうるという証明でした。（直接の影響）

証明という数学の伝統。 「計算機科学」が存在する前に数学者・物理学者として訓練を受けたダイクストラは、証明という基準をまるごと持ち込みました。彼にとってプログラムは数学的対象であり、問うべきは決して「これは動くように見えるか？」ではなく「これは動かざるをえないと実証できるか？」でした。（形成期の影響）

彼が形づくった人々

構造化されたコードを書くすべてのプログラマー。 日々のプログラミングからのgotoの消滅、順次・選択・反復という構成の普遍性、そして並行性の語彙全体——セマフォ、デッドロック、相互排他——は、それ以降に書かれたあらゆるコードベースの中で目に見えず働いている、彼の遺産です。

形式手法とプログラム検証。 述語変換子の計算法と、構成による正しさという理想は、現代の検証、モデル検査、証明付きコードの直接の祖先です。形式的に検証されたシステムソフトウェアの昨今の復活は、ダイクストラの主張が、それを走らせるのに十分な速さのハードウェアについに巡り会ったということです。

この分野の自己像。 どんな個別の成果物にもまして、ダイクストラは、プログラミングが厳密さに値する応用数学の一分野であり——試行錯誤で学ぶ手仕事ではない——という考えを確立しました。この分野の良心は、良くも悪くも、いまなお彼の調子で語っているのです。

貫く一本の筋

ダイクストラは、このシリーズの残りが流れ出す源です。リーナス・トーバルズの「良いセンス」——特殊ケースが消える書き直し——は、ダイクストラの「単純さ＝正しさ」を、カーネルハッカーの語法で言ったものです。分岐が少ないとは、間違いうる箇所が少ないということ。ジョン・カーマックの高速で単純な核は、証明ではなくハードウェアの天井に狙いを定めた、同じ引き算です。そしてアンドレイ・カルパシーが、システムを真に理解するためにはゼロから作り直すべきだと主張するのは、ダイクストラの「紙も鉛筆も使わない設計」が深層学習の帽子をかぶった姿です。この4人はほとんどすべてについて意見を異にしますが、肝心の一点だけは一致しています——優雅な構造は、正しい解の上にあとから乗せるものではない。それこそが正しい解なのだ、と。（シリーズの橋渡し）

私がここから受け取るもの

私が何度も立ち返る一行は、あの逆転です——単純さとは、信頼性を達成した後に手に入れる報酬ではなく、信頼性の前提条件である。遅くて脆いソフトウェアのほとんどは、誰かがテストを省いたから遅くて脆いのではありません。誰一人として、それを理解できるほど小さくしなかったから遅くて脆いのです。だから誰もそれについて推論できず、だから取りうる唯一の品質戦略は、目に見えるバグが出なくなるまでテストすることだけになる——そしてそれは、ダイクストラの言うとおり、何も保証しません。この逆転は、品質こそが唯一の変数であるというのと同じ基準です——問うべきは決して「テストは通ったか？」ではなく「これが正しいと分かるほど、私はこれを十分に理解しているか？」なのです。

私がいま身を置いている世界——AIエージェント、ツールのループ、どんな人間が読めるよりも速くコードを生成するシステム——では、ダイクストラの警告はかつてないほど鋭く突き刺さります。エージェントが千行を書き、テストが緑になったとき、それはまさに彼が描き出した状況です——バグの存在は示されておらず、その不在は示しえないのです。ダイクストラ流の一手とは、生成が増えていくにつれて理解が縮んでいくのを拒むことです——システムを、誰かがなお正しいと証明できるくらい小さく、十分に階層化され、十分に読み解けるものに保てと主張することです。この規律こそ、誰もコードを読まないときでさえ、私が検証の層を構造を支える荷重材として扱う理由です——テストは存在を示すのであって不在を示すのではなく、緑のチェックマークの波面は証明ではないのです。

FAQ

エドガー・ダイクストラのエンジニアリング哲学とは？

ダイクストラは、単純さは信頼性の前提条件であると考えました——プログラムは人間が完全に理解できるほど単純でなければならない、なぜなら理解可能なプログラムだけが推論の対象となり、正しいと証明できるからです。彼は、プログラムは「デバッグによって正しさへ至らせるのではなく、正しく構成される」べきであり、テストはバグの存在を示すことはできても不在を示すことは決してできず、優雅さは装飾ではなく「しばしば成功と失敗を分ける要因」であると論じました。彼の見方では、巧妙さは悪徳でした。それが人間の精神の限られた容量を超えてしまうからです³⁵⁸⁹。

エドガー・ダイクストラは何を発明したのか？

ダイクストラは、彼の名を冠する最短経路アルゴリズム（1956年構想、1959年発表）を発明し、並行プロセスを協調させるためのセマフォとP操作・V操作を導入し、階層化されたTHEマルチプログラミングシステムを構築し、食事する哲学者の問題を定式化し、構造化プログラミングを推し進め、分散システムにおける自己安定化の概念を生み出し、プログラムをその正しさの証明と同時に導き出すための述語変換子／最弱事前条件の計算法を（『プログラミングの規律』、1976年で）発展させました。彼は1972年にACMチューリング賞を受賞しました⁴⁵。

「テストはバグの存在を示すことはできても、不在を示すことはできない」とはどういう意味か？

それは、テストはバグを発動させることによってバグが存在することを実証できるだけであって——バグが存在しないことは決して実証できない、という意味です。なぜなら、有限個のテストの集合では、ありうるすべての入力を網羅できないからです。ダイクストラはこれを1969年のNATOソフトウェア工学会議で述べ、「構造化プログラミングに関する覚書」で規範的な長い形を与えました。「プログラムのテストはバグの存在を示すために使うことはできるが、その不在を示すために使うことは決してできない！」。彼の結論は、正しさへの確信は、合格したテストを積み重ねることからではなく、証明から、そして推論できるほど単純なプログラムを設計することから来なければならない、というものでした²⁹。

なぜダイクストラは手書きで書き、EWD手稿をコピーで回覧したのか？

EWDは、ダイクストラがおよそ40年にわたって書いた1000点を超える番号付き手稿の連なりで、大半は万年筆による手書きで、それをコピーして少数の仲間に郵送し、仲間はそれを複写してさらに転送しました。取り消しキーのない手書きでゆっくり書くことは、紙も鉛筆も使わずにアルゴリズムを設計する彼の習慣と同じ規律を強いました。それは明晰さを強い、ごまかしを罰したのです——インクの上に確定された議論は、実際に成立しなければならなかったからです。全シリーズはアーカイブ化され、テキサス大学オースティン校で自由に閲覧できます⁶¹⁰。

出典