AI ファースト開発、コーディングガードレール、使い捨て前提のアーキテクチャを探求します。
大規模言語モデルはtest oracleの発見において悪くないブレインストーミングパートナーだが、性質を幻覚し、ドメイン制約を見落とす。それらを、怪しいテストをリリースすることなく使う方法を解説する。
事前に正しい出力がわからない関数をテストする必要がある。経路最適化器、感情分類器、物理シミュレーション。Metamorphic testingについて読んだ：入力と出力の間に成り立つはずのrelationを見つけ、正確な値の代わりにそれらのrelationをテストするのだ。…
すべてのmetamorphic relationsがバグを捉えるわけではない。弱いrelationは虚偽の自信を与え、強いrelationだけが本当の欠陥を見つける。どう違いを見分け、実際に機能するrelationセットを構築するかを解説する。
価格設定エンジン向けに12個のmetamorphic relationsを書いた。すべてのテストが通過した。カバレッジに自信を持っている。…
Metamorphic testingを使えば、正しい出力が何かを知らなくてもコードの正しさを検証できる。その仕組み、限界、そして使い始める方法を解説する。
機械学習モデルをリリースした。サポートチケットにラベルを付与するものだ。テストスイートはグリーンだ。すべてのテストが通過した。…
Phantom typesと `this` パラメータを使い、違法なプロトコル遷移を実行時のバグではなくコンパイルエラーに変える方法。
すべてのAPIクライアントの内部には、state machineが隠れている。まずhandshake。次に認証。三番目にデータ送信。最後に切断。この順序を崩すと、実行時エラー、混乱したサーバー、あるいはより悪いことに、静かなデータ破損が起きる。…
OpenAPIの仕様はリクエストとレスポンスのスキーマを記述するが、有効なメッセージの順序までは規定しない。ここでは、どこまで自動抽出できるか、そしてどこに手作業で補う必要があるかを説明する。
OpenAPIの仕様は、有効なリクエストがどのような形をしていて、有効なレスポンスがどのような形をしているかを教えてくれる。しかし、 を の前に呼び出してもよいのか、 の後に を呼び出したらどうなるのかまでは教えてくれない。その情報はプロトコル仕様に存在し、OpenAPIはプロトコル仕様ではない。…
セッション型は通信プロトコルを型システムにエンコードし、実行時のプロトコルエラーをコンパイル時のエラーに変換する。プロダクションコードが使用できるようになるまでに30年間の研究論文に費やされた理由はここにある。
セッション型は1993年に発明された。30年後、ほとんどのネットワークサービスはまだプロトコルの状態を手書きの実行時チェックで検証している。そもそも検証しているかどうかすら怪しい。型システムは、クライアントがの前にを送信したかどうか、あるいは誰かが閉じるのを忘れたために接続がリークしたかどうかについて、何も言わない。…
セッション型は通信プロトコルを型システムにエンコードし、コードが実行される前にメッセージパッシングの不一致をコンパイルエラーに変える。
デッドロックは実行時の問題であるはずだ。だからこそ厄介なのだ。コードはきれいにコンパイルされ、テストも通過し、そしてプロダクションでプロセスAがプロセスBを待ち、プロセスBがプロセスAを待つために動きを止めてしまう。…
Inferを使ってCIパイプラインで形式的静的解析を実行する方法。動作する設定と現実的なトレードオフを紹介する。
抽象解釈は、エンジニアがタブを閉じてしまうような言葉だ。束理論を一学期学ばなければ理解できないようなものに聞こえる。ほとんどの開発者は、それが研究論文の世界のもので、プルリクエストの世界のものではないと思い込んでいる。…
大規模言語モデルは静的解析の偽陽性の選別に役立つが、抽象解釈のようにプログラムの意味論を理解しているわけではない。両者を組み合わせる方法を解説する。
あなたの静的解析ツールは金曜日の午後に847件の警告を出力した。統計的には、そのうち5%から15%が実際のバグだ。残りは偽陽性だ：生成コード内のデッドストア、ツールには怪しく見えるが人間には明らかなヌルチェック、関係のないハッシュ関数内の整数オーバーフロー。 手作業で仕分けするのは精神的に exhausting…
Facebookがどのように抽象解釈と意図的なunsoundnessを用いて、数百万行のAndroidコードにおける競合状態を大規模に発見したか。
FacebookのAndroidアプリにはパフォーマンス上の問題があった。UIスレッドが仕事に溺れていたが、コードをバックグラウンドスレッドに移すと競合状態が生じた。プロダクションでのクラッシュ。怒ったユーザー。…