ハクソク

世界を動かす技術を、日本語で。

より良いプログラマーになるために、頭の中で小さな証明を書こう

314日前原文(the-nerve-blog.ghost.io)

概要

  • コードを書く速度 と 正確さ を向上させる実践的な思考法の紹介
  • 「頭の中で証明をスケッチする」 という習慣の重要性
  • モノトニシティ や イミュータビリティ など、設計上の考慮点
  • 前提条件・事後条件・不変条件 によるロジックの検証法
  • 変更の影響範囲 を限定し、既存動作の安定性を保つ工夫

コードを書く際の思考法とその効果

  • 難しい問題 に取り組む際は、 自分のコードが意図通り動作するか を頭の中で証明する習慣
  • フローを妨げずにオンラインで実施 するには、 練習と経験 が必要
  • この思考法が身につくと、1回または2回の試行で動くコード が書けることが多くなる
  • 明確な手法は人それぞれ だが、いくつかの代表的な考え方を紹介

モノトニシティ（単調性）の活用

  • モノトニックな処理 は「一方向にしか進まない」特性を持つ
  • チェックポイント の実装例：スクリプトの進捗をディスクに保存し、クラッシュ後も未完了のタスクから再開可能
  • LSMツリー のようなデータベース構造体は、 操作履歴の蓄積と単調増加 を活用
  • Bツリー との比較で、 直感的な理由付けのしやすさ を確認
  • イミュータビリティ （不変性）も類似の考え方で、 値の変更禁止による予期せぬ動作の排除

前提条件・事後条件による検証

  • 前提条件（pre-condition） ：関数実行前に成立しているべき条件
  • 事後条件（post-condition） ：関数実行後に成立しているべき条件
  • これらに基づく単体テストの着想やassertionの導入 による堅牢性向上
  • 前提・事後条件が曖昧な場合も発見できる利点

不変条件（インバリアント）の維持

  • 常に成立すべき条件 を「不変条件」として定義
  • コードを原子的なステップに分割し、それぞれが不変条件を保つことを確認
  • ダブルエントリー会計の会計等式 のような古典的インバリアントの例
  • ライフサイクルメソッドやリスナー による状態同期の実装
  • 実行経路が少ない場合の推論のしやすさ

変更の隔離と影響範囲の管理

  • 既存システムを壊さずに拡張・修正する ことがソフトウェア開発の重要な「クラフト」
  • 「ブラスト半径」 という考え方で、変更の影響範囲を限定
  • 構造的な「ファイアウォール」 による変更の波及防止
  • Nerve のクエリエンジンを例に、 依存フィールドの過剰取得と後処理で設計変更を最小限に抑える方法
    • クエリプランナーとクエリエグゼキュータ間の境界 で変更を封じ込め
    • 本質的なロジックは未変更のまま、既存動作の信頼性確保
  • Open-Closed Principle にも通じる考え方

まとめ

  • 頭の中で証明をスケッチする習慣 は、 バグの早期発見と高品質なコード の実現に直結
  • モノトニシティ、イミュータビリティ、不変条件、前提・事後条件、変更の隔離 といった思考パターンを活用
  • 設計・実装時の思考フレームワーク として、日々意識的に使いこなすことが重要

Hackerたちの意見

ああ、関連性があって意外とシンプルな例があるよ：二分探索。二分探索とそのバリエーションである最左端・最右端の二分探索は、ループ不変条件について考えないと正しくコードを書くのが意外と難しいんだ。ループ不変条件のアプローチを[1]で説明したけど、例のPythonコードはできるだけ明確で普通の英語に近いものにしたよ。『Programming Pearls』の著者であるジョン・ベントリーは、IBMのプロのプログラマーたちに普通の二分探索を書く課題を出したんだけど、彼らの実装の90%にバグがあったんだ。最も多かったのは、うっかり無限ループに入ってしまうことだったみたい。公平に言うと、当時は整数オーバーフローに対して明示的に対策を講じる必要があったけど、それにしても驚くべき数字だね。[1]: https://hiandrewquinn.github.io/til-site/posts/binary-search...

└

確かに、インデックスに関して非常に気難しい例を選んでるね。エラーなしで書くのが一番難しい基本アルゴリズムの一つだと思う。ホーアのパーティションと同じくらい難しい。

└

2006年のGoogleの研究論文では、「ほぼすべて」のバイナリサーチ（とマージソート）の実装にバグが含まれていると指摘されていて（何十年も前から）、それを考えると90%はすごいことだと思う。 https://research.google/blog/extra-extra-read-all-about-it-n...

└

有名なバイナリサーチのバグについては本で知ってたし、非常に慎重にバグのない実装を書こうとしたんだけど、結局バグが出ちゃった。:) 幸いにも、マンニングの早期アクセスプログラムのおかげで、印刷前に修正できたよ。

└

二分探索を一度だけ使うんじゃなくて、何度も使うように書く確率ってどれくらい？

└

C++の標準ライブラリでは、二分探索を部分分けの問題として表現してるんだ。つまり、述語が偽から真に変わるインデックスを見つけるってこと。これは自分にとって役立つね。

正しい証明を書くのは難しいよね。プログラムの検証も難しい。個人的には、手作業でやってるならあまりメリットはないと思う。言語やコードベースに合わせたイディオム的なコードを書くと、不変条件や前後条件について考える必要がほとんどなくなることが多いよ。R. パイクとB. W. カーニハンの『The Practice of Programming』をチェックしてみて。モットーは「シンプルさ、明確さ、一般性」。これが日常の仕事で本当に役立つと思う。ちょっと関連する話だけど…競技プログラミングは、コードが正しいことを確実にするための正しい技術を教えるのが意外と得意だよ。これを身につけないと、特定の段階を超えるのは難しい。

└

最初の段落をひっくり返してみて：適切な抽象化（つまり「言語やコードベースに対するイディオム的なコード」）がプログラムの検証を簡単にするんだ。適切に抽象化されたプログラムを手作業で作っているなら、ループ不変条件や前後条件について考えるメリットはほとんどないよ。なぜなら、そのレベルの一般性では存在しないから。正しい証明は正しいコードから直接導かれるんだ。

└

ここには強く反対するよ。OPが言いたかったのは、完全で形式的な証明を考えることじゃないと思う。自分のコードがどんな論理的特性を満たしているのか、例えばどんな不変条件が成り立つべきかを理解しようとすることが、コードの理解をずっと楽にして、恐怖感を減らすことにつながるよ。

└

競技プログラミングのその技術について詳しく教えてくれない？本当に興味があるんだ！ :)

└

正しいプログラムを書くことに代わるものはないよ、どんなに難しくてもね。正しいプログラムが欲しいなら、正しく書かなきゃダメだよ。

└

証明の最も基本的なアイデアは、何かが真である理由を説明することなんだ。小さなミスを避けることじゃなくて、方向性が正しいかどうかが大事なんだよ。

「今のところの私の主張は、『コードについて小さな証明を頭の中で書こうとするべきだ』という感じです。」でも、実はこの投稿には秘密の二重バージョンがあって、「小さな証明を書きやすい形でコードを書くべきだ」と言っているんだ。言うは易し行うは難しだね。最近自分が書いたコードだけのグリーンフィールドプロジェクトでは確かに実現可能だけど、foo()、bar()、baz()をユニット境界を越えて呼び出して、グローバルな状態を変更したり、異なる開発者が書いたりすると、こうやって証明するのはずっと難しくなる。

└

「良い開発者」であるための一部は、システムをこの方向に進化させることができることだよね。実際のシステムはごちゃごちゃしてるけど、以下のことについて考えるべきだし、考えるべきだと思う。1. 不変条件の穴を徐々に減らすこと 2. 成功のための道筋を作ること（後から来るエンジニアが不変条件を理解して、維持するための道を使うように「促される」ようにする）。ドキュメントも役立つけど、コードの構造も重要だよね（経験上、こっちの方が大事だと思う）。

└

それでも、コードベースの「安全な」場所と「危険な」場所のマップを得ることができるよ。つまり、どの関数がグローバルな状態を変更して、どれが変更しないかのメンタルモデルを作れるってこと。

└

君のフラストレーションは実際に示唆に富んでると思うよ。可変のグローバル状態が悪い理由は、そのコードを読むのが正しいかどうかを証明するためには、プログラム全体が何をしているかを知っておかなきゃいけないからなんだ。もし、グローバル変数を不変にして、状態変数を関数の引数にしたり、可変のグローバル状態を何らかのヘルパークラスでラップしたりすれば、特定の関数を呼び出す側が何をしているかだけを知っていればよくなる。そういう関数の可視性は制限できるし、関数内のアサーションで呼び出し側の挙動をさらに制約できる。これらすべてが、リーダーが正しいことを証明しやすくしてくれるんだ。実際、ほとんどのプログラマーはこれをやってると思うよ。ただ、自分の決定をこういう風には考えてないだけなんじゃないかな。

└

foo()、bar()、baz()をユニットの境界を越えて呼び出すと、グローバルな状態を変更したり、異なる開発者が書いたりするので、証明するのがずっと難しくなるよね。この記事のポイントを強調してると思う。こんなコードはバグが含まれる可能性が高いし、バグを増やさずにメンテナンスするのも難しいから、最初から「証明可能性」を目指して書かれたプログラムよりも厄介だよ。

└

グローバルな状態を変更したり、異なる開発者が書いたりする。癌が転移したら、治療計画はより攻撃的で快適ではなくなる。患者は多くの場合まだ救えるけど、それは多くの外的要因に依存するんだ。

大学で理論計算機科学の基礎を学んだよ。この投稿の意見には賛成だけど、実際に実行するのは難しいよね。前提条件や後条件に加えて、ループ不変条件や構造的帰納法はCSの証明において強力な技術だと思う。https://en.wikipedia.org/wiki/Loop_invariant、https://en.wikipedia.org/wiki/Structural_induction トロント大学のCSC236Hのノートは関連性があるよ： https://www.cs.toronto.edu/~david/course-notes/csc236.pdf#pa...

└

そのメモは素晴らしいね。デイビッド・リューは、いい人そうだし。 https://www.cs.toronto.edu/~david/research.html

可変性と不変性も特性のリストに加えたいな。できるだけ多くの状態を不変に保つことは、マルチスレッドにも役立つし、プログラムの可能な状態を理解する際の頭痛を大いに減らしてくれるよ。

└

この記事にはそれも含まれてるよ。

プログラムを証明を意識して設計するべきだって考えは、1959年にT. J. Dekkerが提案した相互排除問題の解決策に遡るんだ。エドガー・ダイクストラがEWD1303でその話をしてるよ。（https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130...）ダイクストラの後の多くの研究は、この洞察の結果を考えていたと言えるね。

昔、大学院の難しい授業で似たような概念に出くわした気がする。学部の後半から、数学のテストをすべてペンでやるようになったんだ。理由は分からなかったけど、ほぼいつも高得点が取れて、きれいな下書きができた。これはその理由だと思ってたけど、実際にはこの投稿が言ってるようなことが助けになってたんだと思う。式を書く前に、頭の中でじっくり考えて、どこに行くかを考えてからペンを持つようにしてた。汚い消し跡を残したくなかったからね。時には、許されるなら捨てる用のメモ用紙を使ったりもした。頭の中で道筋が完全にできたら書き始めて、結果的にミスがかなり減ったよ。コードを書くときはいつもこのアプローチを取るわけじゃないけど、よくどうなるかを頭の中で明確にイメージしてから始めることが多いかな。

あまり話題にならないことの一つは、プログラマーのグループがより良いプログラマーになるために設定できる高レベルの制約やレバーについてだと思う。例えば、アーキテクチャはどれくらい影響があるのか？バグトレース、言語の選択、ツールなど。人々は「これがあれより良い」とか言うけど、各選択肢がコードにどのように影響するかを、個々のコードコンポーネントやその相互作用をグラフやツリーで説明できると、すごく助かると思う。もしそんなリソースを知っている人がいたら、教えてほしいな。

└

今は「このチームリーダーが物事を動かす」段階で、「この戦略が物事を動かす」段階ではないと思う。多くのニュアンスが曖昧だったり間違っていたりする。いくつかの観察を挙げると：1. 人は間違いを犯す。あなたの戦略はそれを考慮する必要がある（レジリエントなランタイム、厳密な型チェック、便利でよく使うREPLなど）。2. プロジェクトの規模が大きくなると、誰もがすべてを覚えているわけではない。あなたの戦略はそれを考慮する必要がある（優れた多面的なドキュメント、コード内での長距離の相互作用を禁止するなど）。3. 依存関係は予想以上にコストが高い、短期的にもね。それを計画する必要がある（より多くのものを外注する、社内でより多くのものを管理する、依存関係管理にリソースを割り当てる、スコープを削減するなど）。まだまだ言えることはあるけど、核心は、プロジェクトの特定の特性は、ある程度の経験がある人には「明らかに」真実だということ。特定の新しい技術について意味のある予測ができる段階にはまだ達していないと思うけど、「これが成功した/失敗したのは{xyz}のせいだ」というメンタルフレームワークは、新しいアイデアが現在の職場にどうフィットするかを考えるのに非常に役立つ。

└

目標は常にビジネスロジックと、他の人が言ったようにアルゴリズムのシンプルさとの間に何らかのシナジーを得ることだ。最良のアプローチは、選んだ言語/環境/ライブラリから始めて、ビジネスルールを表現できるDSLを構築することだ。それがDDDの基本的な前提だけど、ここが複雑になるのはコンテキストを分けて、その境界間の翻訳を行うこと。プログラマーはプログラミング言語理論について少し学ぶべきだと思う。主に言語とは何かについての部分ね。それから、ラベルの背後にあるものを認識し、それらがどのように変化するか（操作からか、コンテキスト間の翻訳からか）を理解すること。そして、その知識を使って環境からビジネスルールを表現できるDSLに移行することが重要だ。アーキテクチャはそのためのドラフトで、出発点と方向性を定義するもの。デザインは、計画に従って決定を下し始めるところだ。目的地のアイデアがある人は、両方を判断できる。

これは「アルゴリズミックにプログラミングする」ということについての直感に似てる。私たちは「アルゴリズム」と「ビジネスロジック」の違いをよく話すけど、根本的には同じことだと思う。どちらも目標を達成するためのステップの計画だからね。私の中では唯一の違いは、プログラムの書き方のスタイルだと思う。「アルゴリズミックにプログラミングする」というのは、望ましくないプログラムの状態を表現できないようにするためのステップを踏むことを意味する。- 検索やソートアルゴリズムの場合、主な関心事は計算速度だから、望ましくない状態は不要な計算や重複計算を行うこと。- 暗号化アルゴリズムの場合、望ましくない状態は暗号化されたデータが漏れること。- 注文の出荷と履行システムの場合、望ましくない状態はすべてのアイテムが配達されていないのに注文を完了としてマークすること。望ましくない状態を防ぐために注意を払うほど、プログラムはアルゴリズミックなスタイルを持つようになる。そして、そうした望ましくない状態が不可能であることを確信する唯一の方法は、証明や不変量の観点で考えることだ。

より良いプログラマーになりたい？そんな馬鹿げた人たちを無視して、毎日コードを書け。それが全てだ。何かを上達させたい？毎日一日中それをやれ。