はい、でも型システムにはドルが何かを教える必要がある
TypeScriptはすべての数値を同一に見なす。ここでは、コンパイラが本番環境に到達する前に通貨換算のバグを捕捉できるよう、USDとEURの違いを教える方法を紹介する。
2022年、大手フィンテックプラットフォームが一括送金32,700,000.00を処理した。この金額は単なるとして保存されていた。下流のサービスはセント単位だと想定した。実際はそうではなかった。…
アイデアとインサイト
AI ファースト開発、コーディングガードレール、使い捨て前提のアーキテクチャを探求します。
数値はただの数値ではない：コンパイラに単位のバグを見つけさせる方法
ミリ秒を要求される場所に秒を渡すようなバグは、どんなテストも通り抜けてしまう。ここでは、単位を TypeScript の型システムに直接エンコードして、実行時コストゼロで混在をコンパイル時に検出する方法を解説する。
ある関数がタイムアウトをミリ秒で要求する。そこに を渡す。後で別の関数がタイムアウトを秒で要求する。そこに を渡す。その間のどこかで を呼び出すと、1時間23分間何も起こらない。 TypeScript はここでは助けにならない。 と のどちらも…
TypeScript が order ID が必要な場所に user ID を通してしまった
TypeScript の型エイリアスは区別された型を作らない。ブランド型は作る。コンパイル時に識別子を混同するのを防いでくれる。
先四半期、私たちは間違った顧客に返金してしまうバグをリリースした。 関数は、order ID を期待していた箇所に user ID を受け取った。文字列は同じに見え、テストは通り、TypeScript は何も指摘しなかった。 両方の識別子は として型付けされていた。TypeScript は両者の違いを見ない。 を…
Differential Testingは形式的証明なしで機能するが、Common-Mode Failureが落とし穴だ
Differential testingを使えば、正解を知らなくてもバグを見つけられる。問題は、相関した誤りが合意に見えることだ。盲点を見つける方法は以下の通り。
形式的証明がなくてもdifferential testingを信頼できるが、その前提はどこで破綻するかを正確に理解していることだ。 その弱点はcommon-mode failureと呼ばれる。specificationのすべての実装が同じ誤った仮定をした場合、それらはすべて合意し、test…
テストでは2つの関数が等価であることは証明できない。では何ができるのか。
N-version programmingは実装が一致することを前提とする。テストがなぜ不十分なのか、SMT solverがいかにして等価性を実際に証明できるのか、そして「十分に良い」と「形式的に検証済み」の境界線をどこに引くべきかを見ていく。
n版システムを構築した。同じクリティカルな関数を3つの独立した実装で用意し、多数決で結果を選ぶvoterを置き、単一障害点を凌駕したという満足感に浸っている。 だが、あなたは関数が等価であることを証明していない。コンパイルが通ることを証明したにすぎない。 n-version…
LLMの複数バリアントが異なる結果を出したら？どちらが正しい？
複数のLLMを並列実行すると、どの単一モデルも見逃すエラーを捕捉できる。実際に機能する不一致解決システムの構築方法を解説する。
GPT-4oにプロンプトを投げる。confidence 0.97のJSON blobが返ってくる。同じプロンプトをClaude 3.5 Sonnetに投げる。異なるJSON…
5つの実装と多数派なし：実際に最良のものを選ぶ方法
N-version programmingは単純に聞こえる。複数の実装を実行して最良の答えを選ぶ。しかし実際には、「最良」を定義することは「最も一般的」を定義するよりはるかに難しい。
同じ関数の5つの実装がある。3つは同じ結果を返す。1つは少し違う。1つは例外を投げる。どれが正しい？ ほとんどのチームは多数決をデフォルトにする。出力が同一でエラーが明らかな場合はうまくいく。しかし、実装が微妙に異なる場合や、すべてのバリアントが異なる答えを返す場合、それは崩壊する。N-version…
同じLLMで関数を5通りに書ける。本当に異なる実装を引き出す方法。
LLMによるN-version programmingに複数のモデルは不要。プロンプト、ペルソナ、推論の制約を変えることで、単一モデルから多様で正しい実装を引き出せる。
N-version programmingでは、多様性は異なる作成者から生まれるものだと想定されている。LLMの場合、それは異なるモデル、異なるプロバイダー、あるいは異なる学習実行を意味する。だがこの前提は間違っている。同じモデルから、問う内容ではなく問い方を変えることで、意味のある多様性を得られる。…
NASAは同じプログラムを27個並列実行した。バグは票を固めて投票した。
N-version programmingは、独立したチームが独立したミスをすると約束した。KnightとLevesonの1986年の実験はその逆を証明し、NASAは静かに撤退した。
1980年代初頭、NASAは今日も safety-critical engineering を悩ませる問いに直面していた：まだ発見されていないバグをどう許容するか？彼らの答えは N-version programming…
Cucumberのシナリオの半分がスキップされている。そのステータスがあなたに嘘をついている理由。
Cucumberの「skipped」ステータスには、全く異なる3つの問題が隠れている。テストスイートを蝕んでいるのがどれか診断し、それを止める方法を解説する。
Cucumberのシナリオの半分がスキップされている。失敗ではない。スキップだ。 その黄色いステータスは、赤いビルドよりも悪い。1つの丁寧なラベルの下に、全く異なる3つの問題を隠しながら、テストスイートを健全に見せかける。スキップされたシナリオは、tag filterが除外したのか、step…