頭の中で小さな証明をしながら、より良いプログラマになる方法

• より良いプログラマになるには、コードを書くときに 頭の中で小さな証明を描く習慣 が重要
• 単調性、不変性、事前条件・事後条件、不変条件などは、このようなミニ証明を行う際の中核となる概念
• コード変更がシステム全体に及ぼす影響範囲（隔離、ファイアウォール）を考慮して設計することは、複雑さとリスクを減らすうえで大いに役立つ
• 帰納法 を活用すれば、再帰関数や再帰的構造の正しさを段階的に証明できる
• こうした思考は練習と習慣化によって育まれ、実際の数学的証明やアルゴリズム問題の訓練が大きな助けになる

---

紹介と核心アイデア

• 筆者は経験を積む中で、コードの正確さと開発速度を高めるために、自然と 「小さな証明を描いてみる習慣」 を身につけた
• コーディング中に予想される動作を頭の中で検証し推論するプロセスには練習が必要だが、習熟するとコードの完成度は目に見えて向上する
• 具体的にどう行うか自体が重要なのではなく、さまざまなやり方で自分に合う形で練習してみればよい

単調性(Monotonicity)

• 単調性 (monotonicity) とは、関数やコードが一方向にしか進まない性質を意味する
• 例としてチェックポイントがあり、これは作業段階が前にしか進まず、すでに終えた作業へ戻って再実行しない
• LSMツリー と対比される B-tree の例では、LSMツリーは大半の領域が蓄積され、コンパクションの過程でのみ減少するという特性を持つ
• 単調性が保証されると、複雑な状態や結果の一部を自然に排除したり予測したりできる
• 不変性 (immutability) も似た概念で、一度設定された値が決して変わらないため、状態変化の可能性を排除できる

事前条件と事後条件(Pre- and post-conditions)

• 事前条件 (pre-condition) と 事後条件 (post-condition) は、関数の実行前後に必ず真でなければならない主張である
• 関数を書く際にこれらの条件を明示的に追跡すると、論理的思考やテストに役立つ
• 事後条件を明確に規定すれば、ユニットテストケースをより容易に導き出せる
• コードにこれらの条件を検証する assertion を追加し、予期しない状況で早期停止するようにすると、予測可能性と安全性が高まる
• 関数にそもそも明確な事前条件・事後条件を与えにくい場合もあるが、それを発見すること自体にも示唆がある

不変条件(Invariants)

• 不変条件 は、コードがどのような状況でも、実行前・実行後・実行中に常に真でなければならない性質である
• 例えば複式簿記の 会計等式 は代表的な不変条件の例である（貸方合計 = 借方合計）
• コード全体を小さな段階に分け、各段階が不変条件を保存することを証明すれば、全体の完全性を確保できる
• 不変条件を維持するために、リスナーやライフサイクルメソッドを使う方法（C++ のコンストラクタ/デストラクタ、React の useEffect など）がある
• 変更点が少ない、または経路が単純なときほど、不変条件の検証ははるかに容易になる

隔離(Isolation)

• 良いソフトウェアの核心の一つは、既存システムを不安定にせずに新機能を追加・修正できることにある
• コード変更の 「影響半径」 (blast radius) を把握し、構造的な 「ファイアウォール」 を作って影響が広がる範囲を最小化しなければならない
• 実際のサービス Nerve の例では、クエリプランナーとクエリ実行器の境界を明確にし、変更された部分がこの境界を越えないよう設計する方法を紹介している
• 不要な変更の波及を防げば、検証と保守が容易になり、安定性も高まる
• これは OCP(Open-Closed Principle) の哲学、すなわち既存動作を変えずに機能を拡張するという考え方にも通じる

帰納法(Induction)

• 多くのプログラムは 再帰関数 または 再帰的構造 を含み、その論理を組み立てる際には 帰納法 が強力に使える
• 再帰関数の動作と正しさを段階的に証明するには、基底(base)ケース と 帰納ステップ (inductive step) をそれぞれ検証しなければならない
• 例として AST（構文木）構造のノード簡約過程を挙げ、各段階の帰納的議論を通じて不変条件の維持と正しい動作を証明している
• 帰納法的な思考が身につくと、再帰コードの作成と検証ははるかに直感的で容易になる
• 帰納的ではない全体的 (holistic) な検証の試みと比べて、どちらの方式がより自然か考えてみる価値がある

Proof-affinity(証明親和性)という品質指標

• 筆者は、「頭の中で小さな証明を描けるコード」 が良いコードだという主張を展開する
• コードが単調性、不変性、明確な条件、不変条件の分割、ファイアウォール境界、帰納法の活用といった構造を持てば、実際に証明しやすくなり、したがってコード自体の品質も高まる
• コードが理解しにくく検証も難しい状態なら、リファクタリングや構造の再考が必要であることを示唆している
• このとき「証明可能性」ではなく proof-affinity（証明親和性）という用語を提案している
• 証明親和性はソフトウェア品質の唯一の要素ではないが、コードの理解・拡張・テスト・保守において非常に重要な促進要因である

実力を高める方法

• このような論理的思考法は、練習を積み重ねてこそ無意識のうちに自然に適用できるようになる
• （数学的な）証明を頻繁に書いてみて、論理的推論力を養うことが不可欠である
• アルゴリズム問題の演習（Stanford の EdX 講義、Leetcode など）も良い訓練の場であり、単なる小手先の問題ではなく、丁寧な実装と証明的思考を要する問題に集中すると効果が高い
• 何度も結果を修正しながら正解に合わせるのではなく、一度で正答に近づこうとする練習が重要である
• このような習慣化を通じて、論理的なシステム設計とコード品質は大きく向上する

[GN⁺]

Hacker Newsの意見

• この話題にぴったりの、単純だが驚くべき例がある。まさに二分探索だ。左端・右端の派生形もあるが、ループ不変条件について考えないと正しく実装するのは非常に難しい。この記事では、不変条件ベースのアプローチと、それに対応する Python コード例を説明している。Programming Pearls の著者 Jon Bentley が IBM のプログラマーたちに普通の二分探索を実装させたところ、90% にバグがあった。主に無限ループに陥るミスだった。当時は整数オーバーフローも自分で防がなければならなかったので、ある程度は理解できるが、それでも驚くべき割合だ

  • これを見て、面接問題として二分探索を使い始めた。よく知られた候補者たちのうち約 2/3 は、20 分以内に正しく動く実装を書けなかった。特に簡単なケースで無限ループに陥ることが多かった。成功した人たちは素早く実装していた。原因の一つは、誤ったインターフェースで学習している場合が多いことだ。Wikipedia の説明も「L を 0、R を n-1 で初期化」としているが、これは R を含む範囲だ。実際には、多くの文字列アルゴリズムでは上限を含まない、つまり R を n にする形のほうがよい。この仮説を自分で実験してみたい。異なる関数プロトタイプと初期値で多くの人に書いてもらい、inclusive と exclusive upper bound、length 方式を使ったときに、どれくらいバグが出るか比較してみたい

  • 実際、二分探索はインデックス管理がほぼ最も厄介な代表例だ。Hoare の分割アルゴリズムと並んで、ミスなく正確に書くのが最も難しい基本アルゴリズムの一つだ

  • 試しに Claude Sonnet にバグのない二分探索の Python コードを書かせてみた

  def binary_search(arr, target):
      left = 0
      right = len(arr) - 1
      while left <= right:
          mid = left + (right - left) // 2
          if arr[mid] == target:
              return mid
          elif arr[mid] < target:
              left = mid + 1
          else:
              right = mid - 1
      return -1
  

  例の配列でさまざまなテストケースも確認した

  • 二分探索のバグが悪いベストプラクティスの代表として有名だと知り、バグのない最初の実装を本に載せてみようと挑戦した。かなり慎重に書いたのに、それでもバグがあって笑ってしまった。幸い、Manning の事前フィードバックシステムのおかげで印刷前に修正できた

  • 私は left/right の二分探索実装を、常に「それまでで最良の値」を覚えながら書いている。C++ の lower_bound、upper_bound のようなやり方だ。while (l < r) 構造で中間点を見つけ、現在位置を確認して適切に範囲を調整する。たとえば upper_bound なら左境界を上げ、lower_bound なら右境界を下げる形だ。久しぶりに leetcode を解いていて頭がぼんやりしているので、フォーマットがひどいかもしれない

• かなり前、大学院の授業でこれに似た概念を知った気がする。学部の最後の頃から、数学の試験は完全にボールペンだけで受けていた。理由はよくわからなかったが成績はいつも高く、一度で解き進めながら、解法の流れを頭の中で完全に描いてから書いていたからだ。そのおかげでミスがかなり減った。コーディングするときも、こういうふうに頭の中で十分に設計してから始めている

• より良いプログラマーになるには、コードに小さな証明を書く習慣を身につけるべきだ テストと型定義はまさにその行為の例だ 特に、まずテスト、その次に型、最後にコードを書く順で取り組んでいる それぞれの acceptance criteria ごとにテストを作り、入力と出力が明確に説明されたテストを書くのが望ましい API なら OpenAPI や GraphQL で、すべてのプロパティと型を含む仕様を先に作れる。実行時にはこの仕様に基づいてデータ検証ができ、この仕様書自体がアプリが仕様どおりに動くことの証明になる 要するに OpenAPI/GraphQL、テスト、型を通じて、システムが実際に意図どおり動くという証明を確保することが重要だ 仕様自体を最初にしっかり設計すれば、コード実装は柔軟に変えても、仕様によって正しさを証明できる コードそのものより仕様のほうが重要だ

  • 記事で触れられていた 5 つの性質は、良い型システムなら表現できる。こうしたやり方によって仕様のかなりの部分がコードになり、コンパイラが正しさを保証してくれる。プログラミングの未来は、こうしたアプローチが当たり前になる方向であるべきだ OpenAPI と GraphQL の型システムはあまりに貧弱で、この未来に到達するにはあと 50 年は発展が必要だろう

• 大学で理論計算機科学の基礎を学んだので、この記事の趣旨には共感する。実践は簡単ではない 事前条件・事後条件に加えて、ループ不変条件(loop invariant) や構造的帰納法(structural induction) のような CS の証明テクニックは非常に強力だ loop invariant、structural induction のリンクとあわせて、UofT CSC236H の講義ノート(講義ノート)を勧めたい

  • この CSC236 の講義ノートは非常に素晴らしいし、David Liu 教授も本当にいい人だ 教授紹介

  • UofT が出てきた！ うれしい気持ちだ

• 「コードについて頭の中で小さな証明を自分で作ってみる」という主張は、自明であるべきほど重要な原則だ。コードの各部分が何をしているのかについての簡単な命題を、常に意識しているべきだ

  • この考え方はグリーンフィールドのプロジェクト（最近自分でコードを全部書いた場合）では簡単だが、さまざまな関数やグローバル状態を複数の開発者が触る現実のコードベースでは、はるかに難しく感じられる

    • 本当に優れた開発者は、システムを徐々にこういう方向へ進化させる能力を持っている。現実のコードはひどいものだが、不変条件の穴を少しずつ減らし、後続の開発者も不変条件を意識しながら、それを保ちやすいコード構造を作ることが重要だ。文書も役に立つが、私の経験ではコード構造そのもののほうがもっと大きな役割を果たす

    • 実際、グローバル状態が危険な決定的理由はここにある。コードの正しさを証明するにはプログラム全体を知らなければならないからだ。グローバル変数を不変値に変える、関数引数として渡す、あるいは状態を包むラッパークラスで管理するようにすれば、その関数の呼び出し元だけを明確に把握すればよくなる。関数内部にアサーションなどで制約をさらに追加すれば、証明の難しさは確実に下がる。すでに多くのプログラマーがこうした判断をしているが、証明を意識せず、本能的にそうしているだけだ

    • 複数の開発者がグローバル状態を管理するコードは、「がんが転移した」患者にたとえられる。治療ははるかに難しく、運や外部条件次第では助けられる場合もある

    • 記事で述べられていたように、こうしたコードはバグが生じる確率がはるかに高く、保守によって追加のバグが入る可能性も大きい。最初から証明可能な構造で書くほうが、はるかに正しい道だと示している

    • この記事を読んで、自分がコーディングのやり方について絶えず考え直し、より良い方向へ再定義しようとしている姿を思い出した。John Carmack のような開発者でも、時間がたつと自分の昔のコードを不十分だったと感じ、もっと「うまく」やっていく感覚があるのか気になる

• コードが証明可能であるべきだという考えは、Dekker が 1959 年に mutual exclusion 問題を解いたときに初めて現れた概念だ。これに関する面白い逸話が Dijkstra の文章 EWD1303(原文リンク)で紹介されている。Dijkstra のその後の研究も、この洞察の延長線上にあると見なせる

• 正しい証明を書くのは本当に難しい。プログラム検証も同じく簡単ではない。私の考えでは、手作業で証明しようとすると効率が悪い。その言語やコードベースにおける慣用的な(idiomatic)コードを書いていれば、不変条件や事前条件・事後条件をあまり気にする必要はない。R. Pike と B. W. Kernighan の "The Practice of Programming" で強調されている「単純さ、明確さ、汎用性」は、実務では非常に大きな効果がある。少し関連はあるが別の話として、competitive programming をやってみると、コードの正しさを保証する技法を確実に身につけないと次の段階へ進めない

  • ここには同意できない。筆者が言っているのは完全な形式的証明ではなく、自分のコードでどんな論理的性質が保証されているのか（たとえば不変条件）を必ず考えろ、ということだと思う。この過程こそがコードを理解し、内容への不安を取り除く最良の道だ

  • ここではむしろ原因と結果が逆になっているように見える。問題を慎重に考えながら取り組めば、その結果としてコードも自然に明快で整ったものになる。論理が明確でなければ、コード設計も明確にならない。しかし、コードをきれいに書いたからといって、それだけで正しさがついてくると信じるのは筋が通らない。もちろん、コードがきれいなほどコードレビューなどでバグが減るのは事実だ。形は機能に従うという点を忘れてはならない

  • 証明の最も基本的な概念は、「これがなぜ正しいのかという根拠」だ。些細なミスを防ぐためだけではなく、根本的に方向性が正しいかを確認する過程でもある

  • コードの正しさのためには、正しくコードを書くこと以外に代わりとなる方法はない。難しくても、とにかく正しく書かなければならない

  • 最初の段落を完全にひっくり返してみると、適切な抽象化（つまりその言語やコードベースに合った慣用的なコード）があれば、プログラム検証は簡単になる。適切な抽象化ではループ不変条件などを考える必要がないため、コードの正しさから証明がそのまま導かれる

• 可変性と不変性(mutable/immutable)も重要な性質だ。状態をできるだけ不変にしておけば、マルチスレッドだけでなく、プログラムの状態推論においても複雑さが減る

  • 元の記事にはすでにそういう内容が含まれている

• 80 年代に Carnegie Mellon の学部生だった頃、こうした原則を明確に教わった。その後の人生で大いに役立っている。特に、再帰と帰納法の同等性を学んだ瞬間、再帰アルゴリズムを「答えが出るまでやみくもに試す」ものとしてではなく、きれいに扱えるようになったのを覚えている

  • 最近その講義を受け、関数型プログラミングを学びながらさらに大きな気づきを得た