2.21 型システムと静的解析

概要と動機

ほとんどの欠陥は、実行時に、テストやユーザーやインシデントによって、遅れて捉えられます。そのうちの一つの種類全体は、そこまで届く必要がありません。型システムと優れた静的プログラム解析のツールは、コードが動く前に読み、ある種の間違いが起こりえないことを証明します。数値が必要な所で使われる文字列、参照を外されるnull、書かれる前に読まれる変数、処理されないまま残されたケース。本章は、正しさを左へ、その行を書く瞬間の近くへ押しやることについてです。そこでは修正のコストが、インシデントレビューの一ページではなく、数秒で済みます。

静的解析とは、コードを実行せずにソースやコンパイル済みのコードを調べる、あらゆる技法です。型チェックは最も広まった形ですが、その仲間には、リンター(様式と正しさのパターンを指摘するツール)、データフローアナライザー、そして遠い端には形式検証も含まれます。共通の約束は、テストを書かず、レビュアーが覚えていることもなく、すべてのビルドで永遠にただで得られる、一種類の保証です。その約束が、この規律が、コーディング標準(2.1章)、ソフトウェア設計原則(2.2章)、テスト戦略(2.4章)と並ぶ理由です。それは、大きなコードベースを安全に変更できるようにする、もう一つの自動化された方法です。

大きなチームにとって、価値は複利で増えます。何百人ものエンジニアが共有のシステムに触れるとき、型のシグネチャは、コンパイラがその全員に強制する契約であり、パイプラインのチェッカーは、疲れず、えこひいきもしないレビュアーです。企業の設定では、型が意図を文書化し、アナライザーが新参者の間違いを捉えるので、これがオンボーディングと統合のコストを削ります。間違った答えが給付を拒否したりデータを露出したりしうる、政府やその他の賭け金の高いシステムでは、機械が確認する保証は証拠です。それは監査人に、欠陥の種類全体が、単にテストされていないのではなく、構造上不可能であることを示します。これは直接、ソフトウェア品質(2.11章)とアプリケーションセキュリティ(4.2章)につながります。

主要原則

正しさを左に押しやる。欠陥を本番ではなく、書くときに捉えます。
人間が覚えておかなければならない規約より、機械が確認する保証を好みます。
意図を型に符号化し、不正な状態がそもそも表現できないようにします。
動的なコードには型を段階的に採用します。すべてかゼロかである必要はありません。
警告をエラーとして扱い、ベースラインをラチェットで改善のみにします。
エディタとパイプラインで、同一のルールで同じアナライザーを動かします。
誤検知は、規律があり、正当化され、レビュー可能な抑制で管理します。

推奨事項

静的型付けか動的型付けかを、目を開いて選ぶ

静的型付けの言語では、型はプログラムが動く前にチェックされ、動的型付けの言語では、チェックされるとしても、動いている間にチェックされます。どちらも普遍的に正しくなく、誠実な枠づけは、保証と柔軟性の取引です。静的型付けは、機械が確認する契約、信頼できるリファクタリング、物が何であるかを知っているツール(オートコンプリート、安全な名前変更、定義へのジャンプ)を買います。動的型付けは、素早いプロトタイピング、簡潔なコード、スクリプトや探索的な仕事に合う低い儀式を買います。システムが大きく、長寿命で、賭け金が高いほど、静的な側が見返りをもたらします。コードベース全体のリファクタリングのコストも、実行時の型エラーのコストも、規模とともに増えるからです。

第二の、直交する軸について正確にしてください。強い型付けと弱い型付けです。強く型付けされた言語は、互換性のない型を黙って強制変換することを拒否します(数値を文字列に加えるとエラーを出す)。弱く型付けされた言語は静かに変換し、"3" + 4が意図しないものになるような驚きを生みます。静的で弱い、あるいは動的で強い、ということもありえます。言語を評価するとき、両方の問いを別々に問ってください。人々が「型付き」と言うとき実際に欲しいのは、しばしば「強い」だからです。

型推論に頼って、型を安く保つ

静的型付けへのよくある反対は、すべての行に型を書く雑音です。型推論はそのコストのほとんどを取り除きます。コンパイラが文脈から型を推測するので、境界(関数のシグネチャ、公開インターフェース)に注釈を付け、内部は推論に任せます。現代の言語は積極的に推論し、動的なコードの簡潔さの多くを保ちながら、静的チェックの安全を与えます。読み手が契約として頼る部分、つまりエクスポートされる関数と公開される型に注釈を付け、ローカル変数は推論に任せる、というハウスルールを採用してください。これはシグネチャを誠実で自己記述的に保ちつつ、内部を散らかしから守り、2.1章の可読性の目標につながります。

不正な状態を表現不可能にする

実用的な型設計における最も強力な考え方は、間違った状態が書き下せないように型を形づくることです。注文が、支払いのない「下書き」か、支払いのある「確定」のどちらかなら、下書きが偶然支払いを持ち、確定した注文が支払いを持たないことがありえる、nullable フィールドを持つ一つの構造体としてモデル化してはいけません。それを直和型(タグ付きユニオン、判別共用体、バリアントとも呼ばれます)としてモデル化します。それぞれが独自のデータを運ぶ、固定された形の集合のちょうど一つである値です。これで無効な組み合わせは存在せず、値を扱うコードは、各ケースを考慮しなければコンパイラが文句を言います。これは実行時の「決して起きないはず」を、コンパイル時の「起こりえない」に変えます。それが要点のすべてです。

同じ本能が、いくつかの日常の道具を駆り立てます。固定された状態の集合には、マジックストリングの代わりに列挙型を使います。検証された値を、別の型で包みます(裸の文字列ではなくEmailAddress)。そうすれば、「未検証の入力」と「検証済みのメール」が、コンパイラが区別して保つ異なる型になります。これは、エラー処理(2.20章)の境界検証の規律の、型システムでの表現です。縁で一度検証し、保証を符号化する型に変換し、内部にそれを信頼させる。

null許容性とジェネリクスを真剣に扱う

ヌルポインタは、その発明者が「十億ドルの過ち」と呼んだもので、かつて静的型システムが嘘をついた、最も一般的な唯一の方法でした。文字列として型付けされた値が密かにnullかもしれず、クラッシュして初めてわかりました。現代の型システムは、null許容性を明示的にすることでこれを直します。値は、決してnullでないStringか、使う前に取り出さなければならないOption/Maybe/nullable型のどちらかで、コンパイラは空のケースの処理を強制します。言語がnullを許さない型やオプショナル型を提供するなら、あらゆる所でそれを使い、裸のnullableを臭いとして扱ってください。これは、本番のクラッシュの一つの属全体を取り除きます。

ジェネリクス、パラメトリック多相とも呼ばれるものは、型の安全性を捨てずに、多くの型にわたって動くコードを書けるようにします。List<T>は、キャストして祈る型なしのものの一覧ではなく、コンパイル時にチェックされる、ある特定の型Tの一覧です。型安全性を保ったまま、再利用可能なコンテナ、関数、抽象化を作るために、ジェネリクスに手を伸ばしてください。直和型、null不許容型、ジェネリクスの組み合わせが、現代の型システムに、プリミティブにタグを付けるだけでなく、本物のドメインのルールを表現させるものです。

既存の動的なコードに型を段階的に採用する

型付けの利益を得るために、動的なコードベースを書き直す必要はありません。段階的型付けは、型付きのコードと型なしのコードを共存させ、最も見返りのある所に型を漸進的に加えられます。今や多くのエコシステムが、これを直接サポートします。別の型チェッカーでチェックされるPythonの型ヒント、動的な言語にコンパイルされる型付きのスーパーセット、既存のランタイムの上に重ねられる型注釈。境界と最も重要なモジュール(お金のコード、セキュリティのコード、データモデル)から始め、チェッカーを寛容なモードでオンにし、時間をかけて締めていきます。古いコードが追いつく間も、新しいコードは型付けされなければならないというルールを加えます。数四半期のうちに、大きな型なしのコードベースは、ほとんどの変更が型チェックされる状態に達し、最も重要な部分が最初にカバーされます。

リンター、型チェッカー、より深いアナライザーを一緒に動かす

型チェックは一つの層で、他の層を加えます。リントのツールは、型チェッカーが無視する疑わしいパターンを捉えます。常に真になる代入、未使用の変数、switchでのフォールスルー、決して閉じられないリソース。より深いアナライザーは、プログラムの振る舞いを推論します。データフロー解析は、値がコードを通ってどう動くかを追跡し、「この変数は代入される前に使われることがあるか」や「このファイルハンドルはエラーの経路で漏れうるか」といった問いに答えます。これらのツールの多くは抽象解釈の上に築かれています。それは、正確な数値の代わりに(たとえば「正」「ゼロ」「負」のような)可能な値の集合にわたってプログラムを抽象的に実行し、一つ一つの実行を走らせずに、すべての実行にわたる性質を証明する技法です。

一部のアナライザーは、セキュリティのツールの隣にあります。静的アプリケーションセキュリティテスト(SAST)は、インジェクション、安全でないデシリアライズ、汚染されたデータが危険な出口に届くといった脆弱性のパターンをソースからスキャンし、ここで述べたデータフローの仕組みを共有します。それをこの仲間の一部として扱い、アプリケーションセキュリティ(4.2章)と調整してください。実用的な推奨は、層をなす集合です。様式と明らかなバグのための速いリンター、契約のための型チェッカー、ドメインにとって重要な性質のための一つ以上の深いアナライザー。ルールが全員に同じになるよう、バージョン管理されたファイルから設定します。

警告をエラーとして扱い、ベースラインをラチェットで締める

ビルドを失敗させない警告は、無視される警告です。ログが何百もの許容された警告で埋まると、誰も読まなくなり、重要な一つが雑音の中に隠れます。新しい警告がビルドを壊し、修正が最も安い瞬間に直されるよう、警告をエラーとして扱う方針を採用します。数千の既存の警告を持つレガシーのコードベースでは、そのスイッチを一晩で切り替えることはできないので、ラチェットを使います。現在の数をベースラインとして記録し、それを増やす変更をブロックし、時間をかけて下げていきます。ベースラインは下がることしかできません。これにより、大規模な前もっての片付けなしに今日厳格なルールをオンにでき、状況が決して悪化せず、着実に良くなることを保証します。

エディタとCIに解析を組み込み、速いフィードバックを得る

静的解析は、フィードバックが即座なとき、最も見返りをもたらします。言語サーバープロトコルかその同等物を通じて、エディタで同じチェックを動かし、開発者が保存する前でさえ、入力しながらエラーを目にするようにします。それから継続的インテグレーション(CI)で同一のルールセットを動かし、通過しなければ何もマージされないようにして、8.1章のパイプラインに結びつけます。両者は一致しなければなりません。エディタが寛容でCIが厳格、あるいはその逆だと、人々は両方への信頼を失います。解析を、すべての変更で実行できるほど速く保ち、結果をキャッシュし、できる所では変更されたものだけを解析して、チェッカーが税ではなく助けになるようにします。エディタとパイプラインが同じルールを同じ方法で徹底するとき、標準は人々が忘れる文書ではなくなり、環境の性質になります。

形式検証は、それに値するコードのために取っておく

スペクトラムの遠い端には形式検証があります。プログラムが、単にテストに合格するだけでなく、正確な仕様を満たすことを数学的に証明すること。技法は、モデル検査(システムの状態を網羅的に探索する)から、定理証明、依存型(完全な仕様を符号化できるほど表現力のある型)にまで及びます。これは利用できる最も深い保証で、作るのが最も高価なので、欠陥が壊滅的な所や、認証がそれを求める所でのみ、その場所を稼ぎます。暗号ライブラリ、飛行制御のコード、ハイパーバイザー、重要なプロトコル。ほとんどのソフトウェアにとって、正しい投資は、強い型と優れたアナライザーで、コストのほんの一部で利益の大半を得られます。形式手法(2.12章で紹介)が存在し、その境界線がどこにあるかを知り、必要とするまれなコンポーネントに意図して手を伸ばせるようにしてください。

抑制を誠実に保つ

完璧なアナライザーはなく、信頼されるツールと無視されるツールを分ける規律は、その間違いをどう扱うかです。すべての本格的なツールは、指摘を抑制できます。各抑制が狭く(一行か一つの指摘で、ファイルやルール全体にはしない)、コメントに理由を持ち、他のコードと同様にレビューで見えるようにすることを求めます。ファイルの先頭にある包括的な無効化が、カバレッジが静かに腐る道です。定期的に抑制を監査し、増え続ける山を、ルールが誤って調整されているか、コードに誰かが隠している本物の問題があるかのシグナルとして扱ってください。誠実な抑制はツールの信頼性を保ち、黙った広範な抑制はそれを芝居に変えます。

トレードオフ: 長所と短所

アプローチ	長所	短所
静的型付け	機械が確認する契約。安全なリファクタリング。豊かなツール	前もっての儀式が多い。初期のプロトタイピングが遅い
動的型付け	書くのが速い。柔軟。儀式が少ない	型エラーが実行時に表面化する。リファクタリングが危険
型推論	簡潔さを伴う安全性。注釈の雑音が少ない	使いすぎると推論された型が意図を曖昧にしうる
段階的型付け	漸進的な採用。重要なコードを最初にカバーする	型なしの縁がなお漏れる。部分的な保証
リンターとデータフロー解析	型が見逃すバグを捉える。実行が安い	誤検知。設定しないと雑音
ラチェットを伴う警告のエラー化	新しい問題をブロックする。ベースラインは改善のみ	邪魔に感じられうる。抑制の方針が必要
形式検証	最強の保証。すべての入力について性質を証明する	高価で専門的。正当化されることはまれ

繰り返される緊張は、保証と摩擦です。より厳格な型付けとより深い解析に一段進むたびに、バグの一種類が不可能になる代わりに、儀式、ツールの実行時間、開発者に数分かかるときどきの誤検知が加わります。賭け金と寿命で解決してください。使い捨てのスクリプトやスパイクは、軽く、速く、動的な端を望みます。決済の元帳、権限チェック、政府が十五年運用するシステムは、強い型、層をなすアナライザー、警告のエラー化、そして最も危険な中核にはおそらく形式的な証明を望みます。厳密さを間違いのコストに合わせ、推論と段階的な採用に、摩擦を負担できる範囲に保たせてください。

チームで議論すべき問い

コードベースのどこで、型システムが直近のいくつかの本番インシデントを防いだはずで、私たちはそれを知っていますか。 ほとんどのチームは、証拠が自分たちのインシデントの履歴にあるのに、型付けについて抽象的に議論します。直近の十か二十の本番の欠陥を取り出して分類してください。値があるべき所のnull、境界を越えて渡された間違った形、処理されないケース、ずれていった文字列型の値のうち、いくつあったか。それらはまさに、型チェッカーとリンターがただで捉える欠陥です。インシデントの大きな割合がそのバケツにあるなら、それが起きたモジュールでより強い型付けを行う、具体的な、ドル建ての論拠があります。ほとんどないなら、バグは別の所(ロジック、並行性、要求)にあり、より重い型付けは最も価値の高い動きではないかもしれません。どちらにせよ、意見をデータに置き換えられます。
段階的型付けを採用するなら、どこから始め、「十分に終わった」とは何を意味しますか。 大きな動的コードベース全体でチェッカーをオンにすることは、スイッチを入れることではなくプログラムであり、順序が、成功するか停滞するかを決めます。どのモジュールが最もリスクを抱え(お金、認証、中核のデータモデル)、したがって最初に型に値するか、どれが安定して低リスクで、今のところ型なしのままにできるかを議論してください。バックログを削る間に型なしの表面が広がらないよう、新しいコードのルール(初日から型付き)に合意します。目標を定義します。おそらく、すべての公開関数のシグネチャが型付けされ、すべての境界が型に検証され、重要なパッケージでチェッカーが厳格モードで動く。明確な終わりの線がなければ、段階的型付けは永遠で、半分しかカバーされないものになり、それは両方の最悪です。
静的アナライザーが間違っているときの方針は何で、それはツールの信頼性を保っていますか。 すべてのアナライザーは誤検知を生み、それをどう扱うかが、ツールが有用なままか、苛立ちで無効にされるかを決めます。具体的なケースをたどってください。指摘が本物の誤検知のとき、抑制は狭く、理由とともにコメントされ、レビューで見えますか。それとも誰かがリポジトリ全体でルール全体を無効にしますか。現在の抑制を見てください。いくつあるか、正当化を伴っているか、最後に誰かが監査したのはいつか。説明のない広範な抑制の山は、カバレッジが静かに空洞化していることを意味します。目標は、アナライザーの信頼性を保つ、共有された徹底される規律で、その指摘が反射的に黙らされるのではなく、信頼され、対応されるようにすることです。
どの言語とアナライザーに標準化し、スタックがチーム間で分断するなかで、ルールセットをどう一つに保ちますか。 何百人ものエンジニアが複数の言語で働くとき、すべてのチームが独自のチェッカー、独自のリンタールール、独自の厳格さの設定に流れていくと、保証が静かに破壊されます。あるリポジトリで強制された契約は、次のリポジトリでは単なる提案だからです。相反する引力は本物です。中央の標準化は、可搬なエンジニアと一様な監査の証拠を与えますが、中央から課されたルールセットは、言語のイディオムと衝突したり、独自の設定に良い理由のあるチームを遅くしたりしえます。本番の言語の一覧、各チームが動かすアナライザーとバージョン、ずれが想定ではなく見えるようにルールセットの差分を持ち込んでください。企業や政府の設定では、答えを調達と監査に結びつけます。すべてのリポジトリが継承する、バージョン管理された単一の設定が、監査人が同じチェックがあらゆる所で動いたことを確認できるようにするもので、供給者が自社の職員が満たさなければならないより弱いルールのもとでコードを出荷するのを止めます。
解析はどれだけ速く、人々はどの時点でそれを迂回し始めますか。 チェッカーは、すべての変更で実行されるときにだけ保証であり、編集とビルドのループを苦痛にした瞬間、エンジニアはそれを飛ばし、ローカルで無効にし、赤いままマージして後で直すと約束することを学びます。緊張は深さと速度です。より深いデータフローやセキュリティのパスは、速いリンターが見逃すバグを見つけますが、フルスイートに20分かかれば、人々はそれを待つのをやめ、誰も待たないチェックは何も守りません。議論に本物の数字を持ち込んでください。エディタのフィードバックのレイテンシ、解析ステージのCIの経過時間、キャッシュのヒット率、チェックを飛ばしたり上書きしたりしてビルドがマージされる頻度、実行のどれだけが増分でどれだけが全体か。大きな、あるいは公的な組織では、計算の請求とスループットのコストを加えてください。フリートの規模では、遅い必須の解析ステージは、予算の項目であり、すべてのリリースを遅らせる待ち行列であり、誠実な修正は通常、ルールを静かに緩めるのではなく、増分解析とキャッシュです。
監査人に実際に出せる機械が確認した証拠は何で、それは重要な不変条件のどれをカバーしていますか。 規制された、賭け金の高いシステムでは、型付けと静的解析の要点は、日々のバグを防ぐことを超えて、欠陥の種類全体が構造上不可能であることの実証可能な証明であり、どの不変条件がどこで徹底されているかを示せなければ、その主張は価値がありません。トレードオフは範囲とコストです。より多くを証明する(あらゆる所でのnull不許容、すべての合法な状態の直和型、中核の計算の形式検証)ことは、より強い証拠を買いますが、厳密さの一段ごとに、注釈の労力、専門家の時間、リスクの低いコードには必要ないかもしれないビルドの複雑さがかかります。安全が重要なモジュールのマップと、それぞれが現在持つ保証、正当化を伴う未解決の抑制のリスト、重要なルールがコンパイラではなく規約によって徹底されているギャップを持ち込んでください。政府や規制された企業では、これを認証の証拠として枠づけます。監査人は、要求される性質を、機械が確認した型や証明までたどれ、あらゆる例外を文書化する抑制のログを見られるべきで、コンプライアンスが、事後の手作業のレビューではなく、ツールチェーンが生成する成果物に拠るようにします。

セクター別の視点

スタートアップ。 速度が勝つので、遅くしない最も安い安全に手を伸ばしてください。強く型付けされた言語か寛容なモードの型チェッカーと、エディタの速いリンター、そしてお金と認証のコードを最初に型付けする。形式検証と深いデータフローのスイートは完全に省きます。持っていない時間がかかるからです。早期に欲しい見返りは、1万行で信頼できるリファクタリングなので、コードベースが大きくなりすぎて手なずけられなくなる前にチェッカーをオンにしてください。

小規模事業者。 静的解析の専門家はいないので、調整して世話をしなければならない一式ではなく、良い既定が組み込まれた言語とツールチェーンを好みます。自前のプラットフォームを立ち上げる代わりに、IDEとホスト型CIに組み込まれた解析を買い、契約者や新規採用者が見分けられるよう、ルールセットをコミュニティ標準に近く保ちます。警告のエラー化と小さな型付きの中核は、限られた予算でできる最もてこの効く動きです。

大企業。 仕事は多数のチームにわたるガバナンスです。すべてのリポジトリが継承するバージョン管理された設定一つ、エディタとパイプラインで同一のルール、そしてどのチームのカバレッジも静かに落ちないようにするラチェットされたベースライン。アナライザーを標準化し、型のカバレッジと抑制の数をポートフォリオの指標として追跡し、機械が確認する保証が監査人の頼れるほど一様に保たれるよう、決まった周期で抑制を監査します。共有の設定を所有するプラットフォームチームに予算を割り当ててください。何千人ものエンジニアにわたる一貫性は、自ら維持されるものではないからです。

政府。 調達、透明性、長い寿命が支配します。契約で、供給者が自社の職員と同じ解析ルールを満たし、設定と抑制のログを成果物として引き渡すことを求め、保証がベンダーの交代を生き延びるようにします。適格性と支払いのロジックには、手作業の保証より機械が確認する証拠を好み、形式検証は失敗すると給付を違法に拒否することになる計算のために取っておき、システムが稼働する十年以上にわたって、すべての抑制を監査のために文書化しておきます。

事例

スタートアップ。 6人のスタートアップは、速度のために動的な言語で製品を構築し、それは、1万行でのリファクタリングが、本番でしか見つからない実行時の型エラーを引き起こし始めるまでうまくいきます。彼らは段階的型付けを採用します。寛容なモードで型チェッカーをオンにし、中核のドメインモデルと決済のコードから型ヒントを加え、すべての新しいモジュールは完全に型付けされなければならないというルールを設けます。チェッカーとリンターを同一の設定でエディタとCIに組み込み、新しい警告をエラーとして扱い、既存のものを下げるようラチェットします。二四半期のうちに、形の不一致によるクラッシュは消え、リファクタリングは怖くなくなり、新規採用者のオートコンプリートはすべての関数が何を返すかを実際に知っています。その投資は数エンジニア週のコストで、顧客向けのバグの繰り返し発生する源を取り除きました。

大企業。 世界的な銀行が、何千人ものエンジニアにわたって静的解析を標準化しています。すべてのリポジトリが共有の設定を継承します。厳格モードの型チェッカー、リンター、データフローアナライザー、セキュリティのパターンのためのSASTスキャナーで、すべてエディタで動き、パイプラインで徹底されるので、通過しなければ何もマージされません。ドメインの型は、お金を動かすコードで不正な状態を表現不可能にします。計上されたトランザクションと保留中のものは異なる型で、通貨は型付けされているのでドルをユーロに加えることはできず、検証済みの入力は生のものと別の型です。警告はエラーで、各チームのベースラインは下がることしかできません。抑制には正当化が必要で、四半期ごとに監査されます。保証が機械で確認され一様なので、監査人は欠陥の種類全体が構造上不可能であることを確認でき、エンジニアは見慣れないサービスの間を自信を持って移動できます。

政府。 国の税務当局が、何年も正しく説明可能でなければならない給付計算システムをモダナイズします。中核の適格性ロジックは、ドメインモデルがルールを符号化する、強く型付けされた言語で書かれています。申請者の状態はすべての合法なケースをカバーする直和型で、金額は個数と混同できない専用の型で、欠けうる値が裸のnullableのまま残されることはありません。静的解析はCIでゲートとして動き、最も安全が重要な計算モジュールは、主要な不変条件がすべての入力について成り立つことを証明するために、形式手法でも追加でチェックされ、認証の要件を満たします。すべての抑制は監査のために文書化されます。元の作者が去ったとき、後任者は、契約がコンパイラによって徹底されているコードを引き継ぐので、十年後でも安全に変更できます。

ビジネスケース: 動機、ROI、TCO

型付けと静的解析の見返りは、欠陥に支払う場所の移動です。エディタで型チェッカーに捉えられた欠陥は数秒のコストで、同じ欠陥が本番で捉えられると、インシデント、調査、場合によっては顧客への被害と規制上の指摘のコストがかかります。欠陥の経済学の研究は一貫して、バグが生き延びる各段階、書くとき、レビュー、テスト、本番で、コストが桁違いに上がることを示しています。静的解析は、欠陥の一つの種類全体を、欠陥ごとの労働なしに、すべてのビルドで、最も安い段階に移します。それは、固定された、大半が一度きりの設定コストが、無制限の防がれた欠陥の流れを買うもので、エンジニアリングにおけるほぼ最良のてこです。

コストは本物ですがささやかで、前倒しです。ツールを選んで設定し、注釈にいくらかの儀式を払い(推論が和らげます)、レガシーコードに段階的型付けを採用するエンジニアの時間を使い、ときどきの誤検知を受け入れます。それに対して、代替の総所有コストを量ってください。本番に届くあらゆる型に由来するバグ、何も正しさを保証しないために避けられたあらゆる危険なリファクタリング、コードが自らの契約を文書化しないために遅いあらゆるオンボーディング、そして規制された設定では、機械が確認する証拠ではなく手作業のレビューで満たされなければならないあらゆる監査。リーダーシップに論拠を示すには、彼らがすでに追跡している指標に結びつけてください。変更失敗率、欠陥の流出率、平均復旧時間、防げた型とnullのエラーに帰せられるインシデントの割合。人々を納得させるグラフは、チェッカーが捉えたかどうかで分類した、自分たちのインシデントの履歴です。

アンチパターンと落とし穴

習慣としての逃げ道: チェッカーを黙らせるためにany、dynamic、あるいは型なしの同等物へキャストすること。保証を、最も必要とした所でまさに消してしまいます。
何もかも文字列型: 状態を本物の型としてモデル化する代わりに、境界をまたいで裸の文字列や型なしのマップを渡し、コンパイラが助けられなくなること。
既定でnullable: 言語がnull不許容型やオプショナル型を提供するのに値をnullableのままにし、十億ドルの過ちを保存すること。
決して失敗しない警告: 何もビルドを壊さないため、重要な一つが見えなくなる、何千もの許容された警告。
エディタとCIの不一致: ローカルでは寛容でパイプラインでは厳格、あるいはその逆で、開発者が両方を信頼せず、マージが人々を驚かせること。
包括的な抑制: 一つの正当化された指摘ではなく、ルールやファイル全体を無効にし、カバレッジを静かに空洞化すること。
解析の芝居: 誰も読まず対応しないツールを動かし、レポートが積み重なって価値がゼロであること。
すべてかゼロかの型付け: すべてを一度に型付けできないから始めるのを拒み、重要なコードを最初に型付けする大きな利益を逃すこと。
どこでも検証: 普通のコードに形式手法を使い、強い型で足りたはずの所に、乏しい専門家の労力を費やすこと。

成熟度モデル

レベル1、開始: 型付けと解析は場当たり的で開発者ごとです。動的なコードにチェッカーがないか、静的な言語が警告を無視して動いています。型に由来するバグ(null、間違った形、処理されないケース)が定期的に本番に届き、正しさを検証するものがないため、リファクタリングは恐れられます。
レベル2、発展: リンターと、関係する所では型チェッカーが一部のプロジェクトで動きますが、ルールはチーム間で異なり、警告はビルドを失敗させず、逃げ道と広範な抑制が一般的です。ある程度の恩恵は得られますが、カバレッジは一貫せず、ツールへの信頼はまだらです。
レベル3、標準化: 共有のバージョン管理された設定が、組織全体で同一のルールで、エディタとCIで型チェックとリンティングを徹底しています。警告はラチェットされたベースラインを伴うエラーで、null許容性と直和型が境界で不正な状態を表現不可能にするために使われ、すべての抑制は文書化されレビュー可能な理由を必要とします。
レベル4、管理: 解析がベースラインに対して測定され、制御されています。重要なモジュールの型のカバレッジ、警告の数、誤検知率、抑制の数、チェッカーが捉えたはずの本番インシデントの割合が、すべて明示的な目標に対して追跡されます。指標が変更をゲートします。お金と認証のコードのカバレッジは落ちられず、上がる誤検知率はルールの再調整を引き起こし、ダッシュボードは、保証が単に設定されているだけでなく、実際に成り立っているかを示します。
レベル5、オーケストレーション: 解析は継続的に改善され、組織全体に統合されています。段階的型付けは重要なモジュールに達し、データフローとセキュリティのアナライザーは日常的に動き、ルールは言語と脅威の進化に応じて適応し、形式検証は、失敗すると壊滅的になる少数のコンポーネントに意図して適用されます。ツール、指標、ルールセットは、設計、採用、調達にフィードバックされるので、組織全体が変更するのにますます安全になります。

議論のためのアイデア

最近の本番のバグのうち、型チェッカーやリンターが捉えたであろうものはどれで、それは全体のどれだけの割合ですか。
ドメインモデルのどこで、直和型や検証済みのラッパー型が、実行時の「決して起きないはず」をコンパイル時の「起こりえない」に変えられますか。
明日警告をエラーにしたら、いくつがビルドを壊し、片付けの十字軍なしにこの方針を採用できるベースラインとラチェットは何ですか。
エディタとパイプラインはまったく同じルールを動かしていて、それらがずれたとき、開発者はどうやって知りますか。
今コードベースにいくつの抑制があり、いくつが正当化を伴い、最後に監査されたのはいつですか。
システムに、失敗が形式検証を正当化するほど壊滅的なコンポーネントはありますか。そしてそれをどうやって知りますか。

要点

静的型付けと解析は、欠陥の一つの種類全体を、修正が最も安い瞬間、つまりコードを書くとき、すべてのビルドで、欠陥ごとの労働なしに押しやります。
人間が覚えておかなければならない規約より、機械が確認する保証を好み、意図を型に符号化して、不正な状態がそもそも表現できないようにします。
すべてかゼロかは必要ありません。段階的型付けにより、残りが追いつく間に、重要なコード(お金、認証、データモデル)を最初にカバーできます。
警告をラチェットされたベースラインを伴うエラーとして扱い、エディタとCIで同一のルールを動かし、抑制を狭く、正当化され、監査されたものに保ちます。
厳密さを賭け金に合わせます。ほとんどのシステムには強い型と層をなすアナライザー、形式検証は失敗すると壊滅的になるまれなコンポーネントのために。

参考文献とさらなる読み物

Benjamin C. Pierce, Types and Programming Languages
Simon Peyton Jones (ed.), The Implementation of Functional Programming Languages
Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Principles of Program Analysis
Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”
Scott Wlaschin, Domain Modelling Made Functional
Steve McConnell, Code Complete: A Practical Handbook of Software Construction
Michael Barr and the MISRA Consortium, MISRA C: Guidelines for the Use of the C Language in Critical Systems
Al Bessey et al., “A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World,” Communications of the ACM