「冷蔵庫も検証すべき」正しいソフトウェアを書く難しさが話題
姉妹サイトの新着
Hacker Newsで「正しいソフトウェアを書くことがなぜ難しいか」という記事が話題になり、ハルティング問題の用語が現代のプログラムの実態とズレてきているという指摘から議論が広がった。コメント欄では、ワープロやブラウザのような身近なソフトウェアの正しさをどこまで証明できるかという現実的な疑問や、計算機科学とソフトウェア開発は別物なのにまとめて語られてきたという不満が交わされた。さらに「計算機科学者とコンピュータの関係は天文学者と望遠鏡の関係のようなもの」という比喩を巡っては、妥当だとする声と的外れだとする反論が分かれた。
正しいソフトウェアを書くことがなぜ難しいか
出典: pron.github.io / 元記事はこちら
"halting problem"(停止性問題)という用語、今となっては古い気がする。最近のプログラムは終了しないものが多いから、"halting"と言われると「計算できなくなった」つまりハングした/デッドロックした、という意味に聞こえてしまう
バイブコーディング界隈で「正しさなんてそもそも存在しないのかも、自分のマシンで動けばそれでいい」って考えが普通になってるの、好きだなあ(呆れを込めて)
本当に知りたいのは、普通のプログラムについて正しさを証明できるのかということ。証明できないプログラムが存在することは知ってるけど興味がない。自分が気にするのはワープロやブラウザみたいな身近なソフトだ。スクリプト言語の範囲を制限すれば、それらを証明できるんだろうか
>>7 それが全てじゃないのは確かだけど、信頼できるコードの土台として純粋関数より良いものを見たことがない。自分のコードがCORSを触ったり環境変数を読んだり.sshディレクトリを覗いたりするのは構わないが、importしたモジュールにそれをさせたくはない
>>2 今年学んだのは、冷蔵庫も検証すべきだということだ
>>10 というか、そもそも冷蔵庫をLANに直接つなぐこと自体をもっと真剣に考えるべきだった
>>2 両方を組み合わせられる場合もある。APIそのものは完璧にできても、現実世界への適応はそのAPIを提供するモジュールの内側でやる必要がある
>>5 計算機科学の言葉づかいは、ソフトウェア開発にはうまく翻訳できないことが多い。計算機科学がソフトウェア開発への入り口だと見なされてきたことは、両方の分野にとって大きな不利益だった
>>14 ある教授が昔言っていた。「計算機科学者とコンピュータの関係は、天文学者と望遠鏡の関係くらいのものだ」
>>25 それ、たしかディクストラの言葉だったはず
>>25 「トースターの寓話」を思い出す: https://www.glaver.org/ftp/humor/toaster-fable.txt
ハードウェアエンジニアも同じことを言う。「我々だけがコンピュータをフル解像度で見ていて、ソフトウェアエンジニアはその気持ち悪い実態を隠す抽象化しか見ていない」と
>>14 ブートキャンプの方がもっと害になったと思う。特にそこを出た人が自分を「エンジニア」と名乗り始めるとなると
>>14 それでも、グラフ探索に単純に落とし込めるような問題を解くために作られた酷いコードを、何度も見てきた。この分野は利点の方が多いと思うが、もっと厳しく門番をすべきだと思う
>>15 「素数」のことも、数学者じゃない人は"prime"の意味を分かっていないから…というのと同じで、自分のお気に入りは"normal"と"almost all"だ。「ほとんど全ての実数はnormalである」というやつ
他サイトの新着
>>21 インターネットに何かをつなぐ前に、もっとよく考えるべきだ
>>25 >天文学者と望遠鏡の関係くらいのもの そんなことはない。その教授は天文学についてあまり知らないんだろう
>>25 天文学者は望遠鏡を使うものじゃないの?
>>31 フォン・ノイマンの名言を思い出す。「パラメータが4つあれば象の形を描けるし、5つあれば鼻を振らせることもできる」
>>39 このジョークは計算機科学者と、アーキテクチャ・アストロノート(実際には生計のためにソフトウェアを書く実務者のことだとしよう)を混同している。それが悲しいことに、よくあることなんだ
この話題の背景と論点
元記事はソフトウェアの「正しさ」を形式的に証明する難しさを論じたもので、ハルティング問題はあらゆるプログラムの停止性を機械的に判定するアルゴリズムが存在しないことを示す1930年代の理論的成果であり、現実のプログラムが止まらない設計を好むようになったこととは本来別の話だ。スレで割れたのは、形式手法がワープロやブラウザのような実用ソフトに応用できるのかという射程の広さと、計算機科学(理論)とソフトウェア開発(実務)を同じ「プログラミング」として扱うことの弊害のどちらを重視するかという点。天文学者と望遠鏡の比喩はディクストラの発言とされることが多いが出典は定かではなく、揚げ足取りではなく教育論の比喩として読むのが本来の文脈だ。
※本記事は海外掲示板 Hacker News のスレッド「Why Writing Correct Software Is Hard」から抜粋し、編集部で日本語に意訳したものです。訳文の責任は当サイトにあります。
この記事のリアクション
まだコメントはありません。