プロでも陥る無限ループを回避！アルゴリズムのバグをなくす「頭の中の証明」とは？

昔の大学院の授業で、記事と似た考え方に出くわしたよ。数学のテストでペンを使い始めたら、頭の中でしっかり考えてから書き出すようになって、高得点になったんだ。コード書くときも、どう動くか、どう動かせばいいか、頭の中でハッキリさせてから書くと、間違いが減るって言ってるね。

8年生の時、代数の先生が「宿題をペンでやったら、間違い減るんじゃない？」って言ったらしい。それから45年、数学者になった今も95%はペンで数学してるって。どれだけ役立ったかは不明だけど、書き直しを嫌うから、書く前にもっと考えるようになったのかもね。

大学で理論コンピューターサイエンスを学んだんだ。記事の考えには同意するけど、実践は難しいって。事前条件と事後条件に加えて、ループ不変式と構造的帰納法がCSの証明に役立つって強調してるね。UofTのCSC236Hのノートも関連してるってさ。
https://en.wikipedia.org/wiki/Loop_invariant
https://en.wikipedia.org/wiki/Structural_induction
https://www.cs.toronto.edu/~david/course-notes/csc236.pdf#pa…

あのノートは最高だね。David Liuって人がめちゃくちゃ良い人みたいだぞ。
https://www.cs.toronto.edu/~david/research.html

良いプログラマーになるには、コードに小さな証明を書くべきだって。それってつまりテストと型（Types）のこと。特にテストを最初に書いて、次に型、最後にコードを書くのがいい。OpenAPIやGraphQLでAPIを定義して、その仕様で実行時にデータ検証するのも良い証明になる。コードより仕様の方が大事なんだってさ。

記事の見出しにあった5つの特性は、良い型システムで表現できるって。そうすれば、仕様のほとんどがコードになって、コンパイラがその特性を保証してくれるようになる。OpenAPIとGraphQLは型が貧弱だから、今すぐにはこれに到達できないだろうってさ。

記事にある「頭の中で証明しろ」の裏には、「証明しやすいコードを書け」って意味もあるんだってさ。言うのは簡単だけど、実際にやるのは難しいと。自分で書いた新しいプロジェクトならまだしも、他の開発者が書いたfoo()やbar()、baz()がグローバルステートを変更するような既存のコードだと、証明するのはめちゃくちゃ難しいって言ってるね。

良い開発者であるってことは、システムをそういう方向に進化させられるってことだよ。実際のシステムって結構ごちゃごちゃしてるけど、不変条件の穴を少しずつ減らしたり、後続のエンジニアが不変条件を意識して、それを守るようなコードを書きたくなるような「成功の落とし穴」を作ったりするのって、ちゃんと考えるべきなんだ。ドキュメントも役立つけど、コードの構造の方がもっと重要だと俺は思うね。

うん、俺が「証明親和性」って言ってたのがまさにこれだよ。ちゃんと構造化されたコードベースって、自分が書いてないコードでも簡単に『これって正しい』って確信できるようなものなんだよね。

君のイライラ、よくわかるよ。可変なグローバル状態がダメなのは、それを読むコードが正しいって証明するために、プログラム全体の動きを知らなきゃいけないからなんだ。もしグローバル変数を不変にしたり、状態変数を関数の引数にしたり、あるいは可変なグローバル状態をヘルパークラスで囲んだりすれば、特定の関数の呼び出し元だけ知ればよくなる。関数の可視性を制限したり、アサーションで呼び出し元の振る舞いをさらに制約したりもできる。これら全部で、読み取り側のコードが正しいって証明しやすくなるんだ。ほとんどのプログラマーは無意識にやってると思うけどね。

この方向性は良いんだけど、できることには限りがあるんだよね。一部のコードは自然と関数型になるけど、他のものは本質的に命令型なんだ。たいてい、プログラムのトップレベル（イベントループとか）は命令型で、I/Oとか画面、ストレージみたいな状態を持つ『デバイス』を扱う。呼び出しグラフの『葉』の部分の関数は関数型にできるけど、トップが命令型だと、プログラム全体について推論することはまだ難しいよ。

そうだね、でも、そういう命令型の部分を全部トップレベルに追い出して、他の全てをクリーンに保てるなら、多くのプログラムの構造よりはるかに大きな改善になるよ。

＞foo()、bar()、baz()をユニット境界を越えて呼び出して、それらがグローバル状態を変更し、異なる開発者が書いた場合、この方法で何かを証明するのははるかに難しい。これって、記事のポイントをさらに強くしてると思うな。こういうコードはバグを含みやすく、さらにバグを追加せずにメンテナンスするのが、最初から『証明可能性』を目標に書かれたプログラムよりもはるかに大変なんだ。

実際、形式的に証明されたコードを見てみると、その80%は変更の複雑さを扱いやすいものに減らすことなんだ。これは、実際に証明するプロセスを踏まなくても価値のあることだよね。

俺、すごく古いチケットでコードベースのめちゃくちゃな部分を整理する作業を終えたばかりなんだ。最初は3つのチケットを直すつもりで入ったんだけど、作業中にさらに6つも見つけちゃって、自分で2つも追加で作ったよ。楽に済んだのか、それとも見落としがあったのか、正直わからないな。今やってる別のプロジェクトも似たような感じだよ。『ねぇ、みんな、大規模なメモリリークがあるの知ってた？』って感じ。

＞彼らがグローバル状態を変更し、異なる開発者によって書かれている場合。癌が転移しちゃったら、治療計画はもっと攻撃的で、楽しくないものになるよね。多くの場合、患者はまだ救えるけど、それはたくさんの外部要因に左右されるんだ。

これ読んでて、俺も常に自分のコーディングアプローチを見直して、『正しく』やる方法を何度も学び直してるなって思ったよ。John Carmackみたいな人でも、『ああ、俺は理解した』って感じでいるのかな、それとも彼も『5年前の俺はダメだった、今はもっと『うまく』やってる』って常に感じてるんだろうか。

昔のコードを見直して改善案が浮かぶのは成長の証しだよ。成長が止まるとそういう発想も無くなるから気をつけな。最高のプログラマーでも完璧じゃないんだから、常に向上心を持つべきだね。学びを止めないって考えはマジで大事だよ。

コードベースで「安全な場所」と「危険な場所」をマップ化できるんだよ。どの関数がグローバルな状態を変えるか、変えないか、頭の中で整理できるってことだね。

プログラムを証明ありきで設計する考え方は、1959年のT. J. Dekkerが相互排他問題を解決した時にまで遡るんだ。Edgser DijkstraがEWD1303 (https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130…)でこの話をしていて、彼の後の研究もこの洞察から来てるんだよ。

正しい証明を書くのもプログラムの検証もすごく難しいよ。手動でやるなら意味ないと思うな。もし言語やコードベースに合ったイディオマティックなコードを書けば、不変条件や事前事後条件なんて考えなくて済むか、必要性がグッと減るよ。R. PikeとB. W. Kernighanの「The Practice of Programming」って本を読んでみて。彼らのモットーは「シンプルさ、明瞭さ、一般性」で、これは日々の仕事で超役立つよ。ちなみに競技プログラミングもコードを正しく書くテクニックを学ぶのに意外と良いんだよね。

強く反対するよ。筆者は完全な形式証明を求めているわけじゃないと思うな。でも、自分のコードがどんな論理的性質（例えば、どんな不変条件が成り立つべきか）を満たすか理解しようとすれば、コードはうんと分かりやすくなるし、怖さもなくなるはずだよ。

うん、「もっともらしい証明可能性の維持」って呼んでもいいかもね。想像上の証明すらできないようなコードは、もっと良いコードと切り離して考えるべきだね。

型も一種の部分的な証明になるんだよね。強力な依存型システム以外では、ほとんどの実行時不変条件の証明まではできないけど、型で証明できる範囲だけでもすごく役立つよ。

そうそう、イディオマティックなコードなら、必要な不変条件は自然と備わってるってことだよ。

「The Practice of Programming」は僕も昔買って、今でも関連性が高くて良い本だと思うよ。でも君の主張には同意できないな。君の提案は大事なアドバイスだけど、証明的な考え方をなくすんじゃなくて、むしろ補完するものでしょ。イディオマティックなコードは複雑なアルゴリズムやアーキテクチャの問題を直接解決しないけど、ノイズを減らして本質的な複雑さを際立たせる役には立つよね。

ある程度は補完し合うってのには同意するよ。僕が言いたいのは、良いコードを書けば、頭の中で複雑な論理をこねくり回す必要は最小限に抑えられるべきってこと。心の中でエッジケースとハッピーパスをテストするだけで十分なくらいにね。例えば、最近見た複雑なロジックは、早期リターンを使えばすごくシンプルになったはずなんだ。作者は分かっていても、そのテクニックに慣れてなかったんだろうな。そしたらもっと効率的に考えられたはずだよ。

みんなが低評価したのは、議論を汚さずに自分で調べられたからだよ。答えはイエスで、両方の単語は「idios」、「own」、「self」、「private」と関係があるんだ。

コメントの投票についてコメントするのはやめてね。何の役にも立たないし、読んでてつまんないよ。https://news.ycombinator.com/newsguidelines.html

うん、僕が考えてたのは、証明じゃなくて「証明のスケッチ」みたいなものだったんだ。

最初の段落を逆にして考えてみてよ。適切な抽象化（つまり、言語やコードベースのidiomaticなコード）を使えば、プログラムの検証は簡単になるんだ。
適切に抽象化されたプログラムを手作業で書いてるなら、ループ不変条件とか事前条件・事後条件を考える意味はあんまりないよ。だって、そのレベルの汎用性には存在しないからね。正しい証明は正しいコードから直接導き出されるんだ。

いや、適切な抽象化だけじゃ僕の議論には不十分なんだ。例えばC言語でidiomaticなループを書く方法が一つあるんだけど、それって構築によって必要な不変条件を引き継ぐんだ。
この本を読むことを強く勧めるよ。idiomaticなコードを書く概念について、僕が説明するよりずっと分かりやすく解説してるから。

C言語のidiomaticなループがエッジケースで間違ってるせいで、どれだけバグが見つかってきたかを考えると、それってマジで面白い例だよね。
iからj（含む）まで昇順にsigned intをイテレートするループって、どうやってidiomaticに書くの？
jがINT_MAXのとき、そのループはどうなる？

頭の中で、あるいは紙にでも、小さい証明をスケッチする人でも、そのケースは見落としちゃうだろうね。C言語で算術演算するとき、普通の算術演算じゃないってことを忘れがちだから！

C言語のループはマジで難しいよな。特に終了条件のチェックとインクリメントの順番が厄介だ。do/whileじゃダメで、結局break使うしかない。C言語（や似たような構文の言語）には、この正しい書き方ってのがないんだよな。

俺様が偉そうに言うけどさ、int i = start; do thing_with(i) while (i++ ＜= end);って書けばいいんじゃね？

それも考えたけど、「一般的に」って書いたのには理由があるんだよ。単純な+1とか–1以外じゃ無理だし、ポインタを追ったりする複雑な処理には向かない。余計な副作用も困るし、break使うのが一番だね。C言語の構文が悪いんだよな。他の言語だとこんな問題起きないんだけど。

「一般的に」って言うなら、『Modern Compiler Design』からの汎用的なforループの実装を見てくれよ。goto使ってて複雑だけど、あらゆるケースに対応できるぜ。Dick GruneさんのコードをC言語に書き直したんだ。
// enumerate: print out numbers from “from” to “to”, inclusive, with step size “by”
void enumerate(intN_t from, intN_t to, intN_t by) {
uintN_t loop_count;
intN_t i;
if (by ＞ 0) {
if (from ＞ to) return;
loop_count = (to - from) / by + 1;
} else if (by ＜ 0) {
if (from ＜ to) return;
loop_count = (from - to) / -by + 1;
} else /* (by == 0) */ {
// Maybe some kind of error
return;
}
for (i = from; ; i += by) {
printf(“%d＼n”, i);
if (--loop_count == 0) break;
}
}
慣用的なC言語のforループより複雑だけど、これが汎用解だよ。

あのi++ ＜= endだと、iが最後のループでendより1つ多くなるんじゃない？++i ＜= endかi++ ＜ endが良いと思うんだけどな。終了条件に＜=を使うのは、だいたい間違いが多いから注意が必要だぜ。

やっぱi++ != endが良いと思ったけど、INT_MAXを超えるsigned intの未定義動作（UB）に気づいたわ。C言語の専門家に聞いたら、インクリメントでUBが出ちゃうってさ。だから更新と条件チェックは完全に分けるべきだな。

うん、符号付き整数のオーバーフローを避けるなら、こんな感じに書くしかないだろ。
assert(i ＜= j);
for (;;) {
do_something_with(i);
if (i == j)
break;
i++;
}

コードがきれいだと正しくなるってのは因果関係が逆だろ。問題を丁寧に考えれば、結果としてコードがきれいになるんだよ。きれいなコードが正しいって信じるのは「Cargo cult programming」だよ。もちろん、きれいなコードは大事だし、コードレビューと合わせれば正確性も上がるだろうけどさ。形は機能に従うんだ、逆じゃない。

「証明」ってのは、何か正しいってことを論証するための基本的な考え方だろ。細かいミスを避けるためじゃなくて、方向性が正しいことを示すのが目的だよ。

競技プログラミングのテクニックについて、もっと詳しく教えてくれない？マジで興味あるんだけど！

競技プログラミングでいつも論理はわかるのに、バグが多すぎて時間内に終われない壁にぶち当たってるんだよね。本当にこれってあるあるだわ。

プログラムを正しく書くこと以上に大事なことはないよ。もし正しいプログラムが欲しいなら、正しく書くしかないんだから。当然だよね。

80年代にCarnegie Mellon大学の学部生だった頃、最初のプログラミングの授業で、記事にあるようなこと全部を教わったよ。再帰と帰納の同等性を知ってから、再帰アルゴリズムを作る時の「イライラする試行錯誤」がマジでなくなったのを覚えてるね。

そのコース、去年取ったんだけどさ、関数型プログラミングを学んでたら、マジで良さが分かってきたんだよね。

プロパティのリストに、mutabilityとimmutabilityも加えるべきだと思うな。状態をなるべくimmutableにしておくと、multithreadingでの問題が減るだけじゃなく、プログラムの取りうる状態を把握する時の頭痛の種もかなり減るからね。

記事にはちゃんとそれらも含まれてるよ。

バグ修正のpost-mortemsを読むのがマジで好きでさ。Raymond Chenがよくやってるやつね。最近あったバグはC++でgarbage-collectedなオブジェクトを使うthread-poolでのcrash。最初はconcurrencyの問題だと思ってたけど、結局はlistenerがオブジェクトをちゃんとmarkしてなくて、GCで消されちゃったのが原因だったんだ。ChatGPTはconcurrencyの問題を推してたけど、違ったんだよね。

1991年頃作ったゲームで、時々crashするバグに悩まされたんだ。再現性が低くて困ったから、ゲームの入力とロジックを全部deterministicに書き直してみたの。そしたら、player inputを記録してreplayできるようになって、ついにバグを再現！結局、dangling pointerのせいで、二発目のshotがメモリを壊してたんだよね。deterministicエンジンは当時珍しかったけど、今じゃ普通だよね。

入力全部保存するってのは極端だけど、結果的にはすごい効果あったんだね。いい話だわ。

頭の中で小さな証明を書くべきって、当たり前だよね？コード書くならそうすべきだし、コードの各部分が何をするのか、簡単な目標を持つべきなんだからさ。