Radium Software
2007-07-10
プログラムにとっての「正しさ」って，なんだろう？
僕らは日常的に，このプログラムのこの部分は間違っているだとか，この部分は正しいだとか，この部分にはバグがあるだとか，バグが無いだとか，そういうことを話し合ったりする。でも，ここでいう「間違い」や「正しさ」，それから「バグ」っていうのは，いったいなんのことを指しているんだろう。
ちょっと視点を変えてみよう。たとえば……「完璧に正しいプログラム」，つまり「バグのまったく無いプログラム」を組むことって，はたして可能かな？
僕らは，どんなプログラムにも，多かれ少なかれ，バグが存在するってことを知っている。それは仕方のないことで，どんなに頑張ったとしても，必ずプログラムにバグは混じってしまう。
それに，間違いをおかしてしまうのはプログラミングの話ばかりではなくて，プログラムのもととなる仕様が不完全なものだったり，矛盾を含んだものだったりすることだってある。もとの仕様がダメなものだったら，そこから生まれるプログラムだってダメなものになるのは，仕方がないことなんじゃないかな。
でも……もし，ここに超人的な知性を持つひとがいて，そのひとが超人的な知性と注意力をもって完璧な仕様を作り上げて，そこから完璧なプログラムを導き出したならば……そのプログラムは「完璧に正しい」「バグのまったく無いプログラム」になるかもしれない。
そう思わない？
ああ，なぜかそうは思えないんだな。「バグのまったく無いプログラム」なんてのは，理想とかいうものでもなくて，いわゆるナンセンスのたぐいのような気がする。それを考えること自体に意味が感じられない，っていうこと。
なぜそう思うんだろう――ちょっとそのことについて考えてみよう。
参考文献
Richard A. De Millo, Richard J. Lipton, Alan J. Perlis. Social Processes and Proofs of Theorems and Programs. Communications of the ACM, 22(5). 1988.
Robert Pollack. How to Believe a Machine-Checked Proof. In Twenty Five Years of Constructive Type Theory. Oxford University Press. 1998.
Yves Bertot, Nicolas Magaud, Paul Zimmermann. A proof of GMP square root using the Coq assistant. Rapport de recherche, INRIA. 2002.
2007-07-11
「正しさ」はどうやって確かめることができるんだろう？
たとえば数学なんかは，どうやってその正しさを確かめているんだろう？ 数学は，とても広大で複雑な体系を，論理的な演繹によって築き上げている。論理的な演繹によって動くという理屈ならプログラムも同じこと。それじゃあ，プログラムの「正しさ」も，数学の「正しさ」と同じような理屈で確かめることができるかもしれない――そう思わない？
それじゃあたとえば……ここにリーマン予想の証明を記した論文があると思ってみてほしい。すると，そのことを知ったあるひとが，こんなことを言うかもしれない。
「ああ，これでリーマン予想は証明されて，定理になったんだ」
いやいや，そういうわけにはいかないよね。リーマン予想を証明したとされる論文は前にもいくつか発表されていて，そのたびに誤りのあることが指摘されてきた。今回のだって間違っている可能性はある。まずはそう考えておくのが無難なんじゃないかな。
それじゃあ，どうしたらリーマン予想は証明された定理になることができるんだろう？
それにはまず，その論文が数学者のコミュニティ（学会）に向けて発表されなきゃならない。すると，その論文は多くの専門家の目による精査を受けることになる。そして，そのすべてを通過することができたなら，そのときにはじめて「証明は十分に正しい」ものとして認められることになる。そこまでしなければ，その証明が正しいかどうかなんて，誰にも断言することはできないんだ。
まあ，そんなこんなで，このリーマン予想の証明が正しいと認められたとしよう。
「ううむ，なんだ，この証明は最初から正しかったんじゃないか。学会で認められることなんて待たずに，最初から信じておけばよかったよ」
いやいやいや，そういうわけにはいかないよ！ 「最初から正しかった」なんてことは，誰も言っちゃいないんだ。コミュニティの精査を受けることによって，「数学の体系へ組み入れるのに十分な程度の正しさを持つ」っていう判断が下されただけで，それは絶対的な正しさを意味しているわけじゃない。
「これまでも，そしてこれからも，絶対的に正しくあり続ける」なんて理屈は，なかなか存在するものじゃない。「よっぽどのことがないかぎり，これは正しいということにしておいてよさそうです」という合意を作っては，それを延々と積み上げていっているに過ぎない。数学の体系というのは，そうやって築き上げられてきたものなんだ。
さあ，ここでちょっと考えてみてほしい。けっきょく，この証明の「正しさ」とは，どこからやって来たものなんだろう？
どうもその「正しさ」とは，その証明の中に最初から備わっていたものではないようだ。その「正しさ」とは，論文の執筆者とコミュニティとの間の意見の交換という，社会的な過程の中から生まれてきたものと言えるんじゃないかな？
2007-07-12
それじゃあプログラムの場合はどうだろう？
プログラムの場合も同じで，たとえどんな理屈を持ち出したとしても，そこからいきなり「絶対的な正しさ」を断言したりすることはできないと思うんだ。プログラムが持つべき「正しさ」というのは，そこに関わる人たちの総意のうえに成り立つ「恐らくの正しさ」であって，「絶対的な正しさ」ではない。そこを履き違えてしまうと，ありもしないものを頼りにしてしまったり，得られようのないものを求めてしまったりすることになるんじゃないかな。
たとえば，あるプログラマーに，ある仕様の実装を依頼したとして，その実装が納品されてきたとしよう。そして，そのプログラマーが，こんなことを言ってきたとする――
「いやあ，このプログラムは正しいですから，信じてもらって結構ですよ」
まあ，これは論外だよね。確かめてみないことには，正しいかどうかなんて分かりようがない。
するとそのプログラマーは，こう切り返してくる。
「そこはちゃんと，いくつものテストプログラムを用意して検証しましたから大丈夫ですよ」
ううむ，でも，テストプログラムなんかは，しょっちゅう間違えて書いちゃうものだってことを，みんな知っているはず。間違ったテストプログラムを書いて，間違った検証をしているだけなのかもしれない。つまり，テストプログラムを検証してみないことには，正しい検証が行えているかどうかなんて分かりようがないんだ。
そこでさらに，そのプログラマーは，こう切り返してくる。
「いやあ，そう思って，最新の検証技術であるところの MacroSoft Visual ProofSafe を使って仕様との適合性チェックを行っているんですよ。最新のソリューションが正しさを保証してくれるんですよ」
いやしかし，どんなにその検証ツールが厳格なものだったとしても，そのツールに入力した「仕様の記述」と「本来の仕様」とのあいだに差異があったとしたら，やはり検証は役立たずになってしまうんじゃないかな。だから，まずその「仕様の記述」を検証しなきゃいけないし……それに，そもそも，そのツールはほんとうに信頼できるものなの？
結局のところ，検証のための手法や道具はさまざまに存在するものだけれど，「検証から確信を得る過程」というのは，それぞれの人の心の中で起こるできごとであって，それに対する手法や道具なんてものがあるわけじゃない。もちろん，その確信だけを抜き出して人へ伝えるってこともできない。確信を得たいと思うなら，その過程を自分の中で再現することによって，自分の中から確信を生み出さなきゃならないんだ。
理想なのは，そこに関わるひとたちすべてが，そういった確信を得られる状態にすること。それを無しに，ただ「絶対的な正しさ」を求めてプログラムの中を探し回ってみたところで，最終的に納得のいく結論に辿りつくことはできないと思うんだよね。
2007-07-13
それじゃあ数学を真似すればいいのかな？
けっきょくはプログラムも，どこかに「絶対的な正しさ」が存在するわけじゃなくて，人と人との間のやりとりの中から「恐らくの正しさ」を見つけ出していくしかない……ううむ，それじゃあ，数学がそれをやっているのを真似すれば，プログラムも「正しさ」を確かなものにしていくことができるのかな。
「数学の真似をする」というのは，よさそうなアイデアのように感じられるかもしれない。でも，これを実際にやっていくのはちょっと難しそうだ。なぜなら，「プログラムの検証は数学の検証ほど刺激的なものではない」からね。
数学の定理っていうのは，ものすごく抽象性・一般性の高い概念で，そこからさまざまな分野への応用が生み出されるものなんだ。だから，数学の定理の「正しさ」を確かなものにするという作業は，人々にとってすごく大切なことで，研究者にとってはすごく刺激的なことでもある。
ところがプログラムっていうのは，いわば理論の応用であって，問題の種類としては枝葉に位置するものだったりする。もちろん，それに価値が無いってわけじゃない。でも，個々のプログラムの「正しさ」を確かめることは，数学の定理の「正しさ」を確かめることと比べると，限られた人の興味しか呼ぶことができないし，研究者にとっては刺激の薄いことでもある。
ちょっと具体的な例を見てみよう。ここにフランスは INRIA の Yves Bertot という人が執筆した論文があって， GMP 多精度演算ライブラリの平方根関数の形式的な証明を行っている。もとは 30 行ほどの小さな関数なんだけれど，それの証明に 25 ページほどの紙面が割かれている。なんでも，その実装の形式的な証明の記述は１万３千行にも達するんだそうで，とても人手には確かめようがないので Coq という証明補助ツールを使っていたりする。
これはまさに「数学的な手続きでプログラムを検証してみた」という例になるわけだけれど，この証明をそのまま鵜呑みにすることはできない。ざっと考えただけでも，いくつかの疑問がわいてくる。
おそらく，ちゃんとした数学の知識があって，さらにプログラムの知識があって，あとは多少の根気があれば，この論文を読むことによって，その正しさに確信が持てるかどうかを判断することができるんだろう。でも……はたして，そこまでする人がこの世に何人いるんだろう？
この例はまだましな方で，多精度の平方根関数っていう一般性の高い問題に取り組んでいるから，もしかしたら興味を持つ人が現れてくれるかもしれない。でも，もっと一般性の低い，ごく普通のプログラムについて，検証に興味を持つ人なんて現れるものかな？ そもそも， 30 行の関数を検証するのに 25 ページも使っているのに，実用規模のプログラムを検証しようと思ったら，はたして何ページの紙面が必要になるんだろう？
2007-07-18
それで，けっきょくどうすればいいんだろう？
まあ，これまでの「絶対的な正しさは存在しない」だとか，「数学的なアプローチは難しい」だとか，そういうのは深くつきつめたときの話であって，あまり深刻に考えこむ必要はないと思うんだ。ある程度の正しさだったら，それを確かめるための決まりきった手順は存在するし，数学的なアプローチだって，分野によってはそれが有効にはたらくこともある。
なんにしろ大切なのは「すべての工学的な活動は経済性にもとづいている」ということだと思う。
なにかを実現するための工学があったとして，そこから得られる利益が，それに要されるコストを下回っていたとしたら，それは工学として成立しない。これは分かるよね？
「正しさ」を確かめるにはコストがいる。だから工学としては，限りなくコストをかけて「絶対的な正しさ」を確かめるってわけにはいかない。どこかで見切りをつけないと，それは工学として成立しなくなってしまう。
他方で，「正しさ」が確かめられていなければ，そのぶん運用時のリスクが生まれる。どの程度のリスクが許容されるかっていうのは，その工学が扱う問題の種類によってことなってくる。たとえば，原子力発電所とドリンク自販機では，許容されるリスクの程度がぜんぜん違うよね。
そこで重要になってくるのが，その問題においてどの程度のリスクが許されて，どの程度の「正しさ」が確かめられているべきかっていうことを，その当事者たち，ないしは責任者が判断してコミットする――ええと，「表明を行う」ということなんだ。
そういう合意が無いと，「正しさを確かめる」っていう工程は，ただやみくもに問題の領域をさまよう作業になってしまう。結果として，風が吹くだけで壊れる原子力発電所を作ってしまったり，ミサイルが当たっても壊れない自販機を作ってしまったりしてね……。「そんなばかな！」って思うかもしれないけれど，ソフトウェアの分野によっては，その分野が若くて洗練されていないがゆえに，そういう悲劇が生じてしまうこともあるんだ。
……ああそうだ，それともうひとこと！ ここから，独りで「正しさ」を確かめることの難しさも推し量ってほしい。「正しさ」が当事者たちの合意のうえにのみ成り立つものだとしたら，それを独りでどうにかしろっていう方が無理な話じゃないかな？