[debian-users:12170] Re: historical info

[Mitsuru Oka <oka@debian.or.jp>]

岡＠情報科学.高知大です。# まだ起きてる、やばい...。


"kenn"すなわち"Ken N."さんより:
kenn> ついてくのが結構大変。いや、理論じゃなくて議論のペースに。

ちょっと暴走気味でした...。

kenn> =   岡＠情報科学.高知大です。
kenn> =   # 風呂に入ったら回復したのでもうひと頑張り。

kenn> ＃やっぱり若者は回復が早いなぁ。きっと朝までダイジョーブなんで
kenn> 　しょうね (『え、なにが？』とかって訊かないように B-)

# 先に突っ込まなくても(^^;...。これでも最近睡眠時間の調整に
  必死なんです、もう若いとは言えない...。


kenn> それはさておき、今日の所は先に一点だけ確認させてください。続き
kenn> は明日。

kenn> =   僕はと言うと、以前は Ken N. さん寄りだったんですが、Debian
kenn> =   はそこまで完璧ではないことを知って、むしろ完全性を維持しよう
kenn> =   という行為がシステムを脆くする事に気がつきました。どんなにシ
kenn> =   ステムが正しさを維持しようとしても、アプリケーションレベルで
kenn> =   システムの状態破壊が起きる可能性が充分考えられるからです。

kenn> これは具体的にはどういう場合ですか？
kenn> いえ、別に反論のための反論をしようとするつもりはなくて、ただ、
kenn> そのような可能性については私は全く考察していなかったので、岡さ
kenn> んがどのような可能性に思い当たったのかを教えて頂きたいのです。

確かに具体例が挙がってないですね。

極端な例で構わなければ、今書けます。パッケージとしてインストー
ルされたアプリケーションが致命的なバグを抱えていて、dpkg の
管理管轄のディレクトリに無作法に書き込みをしたり(suid 指定で
root で動くなどが必要ですが)、さらに極端な場合は dpkg が保持
している情報(/var/lib/dpkg 以下)を破壊した場合が考えられます。

それでなくても、大なり小なり、一貫性の破壊は起こり得るような
気がします。アプリケーションがデータベースを作成したものの、
アンインストールされて、データベースが残ってしまったというの
も、システムは不健康な状態にあると言えそうです(普通は purge
の時に postrm あたりで削るのかな)。


kenn> =   これと導出規則等を使えば、プログラムの正しさを証明する
kenn> =   ことさえある程度可能です(当然無限ループとかがネックになる)。

kenn> 純粋な関数なので副作用は持たない、ループは末端再帰に帰結できる、
kenn> 各再帰呼出で事前条件に再帰続行の条件を繰り込み、あとは上手に数
kenn> 学的帰納法に持ち込んで証明終り、そんな感じですか。

仕様記述言語なるものも存在しますが、いづれにしても、口で言う
程に簡単な作業ではないようです、実際の所。国防総省なんかが納
入元の企業に要求してきそうな代物ですね。

# さて、議論がいかに形になるかがネックになりそう...。
--
岡 充 (Mitsuru Oka)
高知大学理学部情報科学科4回生