証明士について：三宅秀道『新しい市場のつくりかた』

このごろ証明士という言葉をつくって、ことあるたびに書くようにしてみたら、あるとき電話がかかってきて電話の先の人が証明士という単語を発音してくれたので、すこしずつ証明士という言葉が広がっているようである。三宅秀道『新しい市場のつくりかた』の最初のあたりに、製品開発ではなく文化開発でウォシュレットは売れるようになったのだという話がある。確固たる作戦無しに証明士という言葉だけ作っていたのだが、どうやらこれは文化開発ということになるらしい。

昔から証明を書くのは数学者だったが、数学者は知らなかったことを知るために証明を書いたり例をつくったりしてきた。証明士は当たり前そうなことを確かめるために証明を書く。ソフトウェアが思ったとおりに動くことを確かめるために証明を書くと、形式検証していることになる。入力が一億通りくらいなら全部テストできるけど、10バイトくらいになったら全通りテストしていると地球が無くなってしまうので、代わりに証明を書いて済ませるのである。

いまの形の形式検証が流行るかどうかは知らない。一部、形式検証を使わないと認証が取れない規格も登場してきているらしいが、規格ごと素通りされるようになる可能性はある。ユークリッドをみればわかるように、形式化オタク的傾向をもった人というのは世の中にいる(本当の形式化オタクは、ユークリッドの原論をみて、正三角形を作図するところで、つまずくはずである)のだが、形式化オタクだけからなる市場では、形式化したくて勝手に形式化する人ばかりいて、その人たちを必要とする存在が感じられない。一つの可能性は、必要はなくても芸事として進んでいくという方法で、ものすごく上手でそれに人生埋める覚悟の人がプロになって、そこまででない人が習い事として証明を書くというものである。そんなに流行るであろうか。

もう一つの可能性は、ソフトウェアを書いたのに証明が書いてないのはなんだか気持ちが悪いとか、数学っぽいことを書いたのに形式化されていないのは、なんだか落ち着かないというように、形式化されていることが当たり前になっている領域をつくることである。そういう領域はちょっとずつ増えている。項書換え系の停止性の議論は、だいぶ形式化されているらしい。目標として数学者というのは、どうもよくない気がする。というのは、ある数学者が若かったころに話をしたら「一度証明できちゃったら他の証明とかぜんぜん興味ないんだよね」とか言っていたので、自分が(ひとつの証明を)わかってしまえばどうでもいいのが数学者だからである。というわけでソフトウェア屋さんを相手にしたい。検証したい問題を解ってもらうだけで手間がかかるのが最大の問題であるから、まあ、かっこいいことを証明したいとかいう欲はしばらく捨てて、それなりに高速なsortとかuniqとか、ごくごく身近な小さなものを検証していって、くだらないことから手当たり次第にやっつけていけばいいのではないか。

新しい市場といえば、ヨーロッパにいくつかNew Marketとかそれに類する地名があった。アムステルダムの南記という中国料理店があったのはNieuwmarktと呼ばれる広場で、蒸し牡蠣のたれがおいしかった。Henry Cecilという人が薔薇を育てさせたり馬と話したりしていたところもNew Marketという名前であったように思う。