sawara__ の回答履歴

近年プログラミングの世界でも VDM(http://en.wikipedia.org/wiki/Vienna_Development_Method) に代表さ れる形式的証明がもてはやされ始めました。 でも私には、プログラムの形式 的証明は、うさんくさいものに思えてなりません。 形式的証明が絶対に不可能だとは思っていません。Goedel の不完全性定理や、 Turing マシンの停止判定問題などから解るように、万能の証明方法を探すの は無駄です。でも、これらの証明不能性は問題の範囲をメタな対象まで含め てしまうことから発生しています。形式的証明の対象範囲を旨く限定してや ればプログラムが仕様どうりに動くことを形式的に証明できることはありう るだろうと思います。 でも一般的に証明問題は難しすぎます。プログラム動作の形式的証明が旨く 機能できる範囲など極端に限られると私の直感は主張しています。 現在でも、プロの数学者が定理や公理を構築する作業は、自分の頭の中での 論理展開をノートに書き残す方法で行っているでしょう。 Coq(http://coq.inria.fr/) なども出てきましたが、このようなソフトを使 っているのは、自動証明の研究者などに限られるでしょう。しばらくは(たぶ ん 100 年以上は)プロ数学者の研究・証明のために行う論理展開作業をコン ピュータが代行することはないと思います。 現実のコンピュータ・プログラムが対象としているのは、数学の世界のよう な綺麗なものではありません。人間が定める膨大かつ不明瞭な仕様書の塊は、 形式的証明の対象にできるとは思えません。たとえできたとしても純粋数学 より難しいはずです。 限られた特殊な領域では、現実のプログラムを形式的証明で扱えるかもしれ ません。でも、そんな形式的証明を理解でき人間は限られるでしょう。大多 数のプログラマーには理解されないでしょう。形式的証明自身に誤りが入り 込んでいないかを検証することは不可能に近い作業になると思います。 私には現実のプログラムが仕様書どうりに動くことを形式に証明することは、 まだ実務的には無意味な作業としか思えません。皆様の御意見を伺わせても らえますでしょうか