LLMはコードの正しさを証明できないが、証明のための定型作業は書ける
クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。
クリーンルーム・ソフトウェア工学では、コンパイルする前にコードの正しさを証明することが求められる。それは立派に聞こえるが、10個の整数をソートする関数のループ不変条件を3時間かけて書いていると、そうは思わなくなる。…
アイデアとインサイト
AI ファースト開発、コーディングガードレール、使い捨て前提のアーキテクチャを探求します。
Cleanroom は 1KLOC あたり 0.1 defect を達成する。フル導入しなくてもそこに到達できる。
Cleanroom software engineering は defect rate を 100 倍に削減するが、フル導入には分離した test team と formal proof が必要。ここでは、overhead なしにその大半の benefit を得られる pragmatism なサブセットを紹介する。
Cleanroom software engineering は 1,000 行あたり 0.1 の defect を達成する。業界平均は 10 から 50 だ。問題は、フルの Cleanroom ではチームを author と verifier に分割し、すべての module の前に formal…
IBMのZero-Defect ProcessはKLOCあたり0.1 Bugを達成した。それでも業界は見捨てた。
IBMのCleanroom engineeringは業界平均より100倍優れたdefect rateを達成し、その後忘れ去られた。消えた理由は、それが機能したかどうかとは無関係だった。
IBMのCleanroom software engineering processは、千行あたり0.1のdefectを達成した。当時の業界平均は10〜50だった。このprocessは文書化され、複数のプロジェクトと言語を横断してreplicateされ、独立して検証された。そして消えた。…
本当に1万行を零欠陥で検証した人がいるのか？IBMはやったし、その方法論は結果より奇妙だ。
Cleanroom software engineeringは、デバッグではなくmathematical verificationによって零欠陥のインクリメントを約束した。我々はIBMの実プロジェクトデータを見て、その主張が成り立ったかを確認する。
1980年代のソフトウェア業界平均は、1000行あたり30〜60の欠陥だった。IBMのCleanroomチームは、2万行のコンパイラインクリメントをテストで53の欠陥を発見した状態で出荷した。これはKLOCあたり2.6である。1万行の個別インクリメントの中には、システムテストで欠陥が全く見つからなかったものもあった。…
あなたのモジュールには3層ある。書いたのは1層だけだろう。
Box Structureは、モジュールが何をするか、何を記憶するか、どう動作するかを、3つの独立した検証可能な層として定義することを強制する。Cleanroomがどうやってデバッグを排除するか、ここで解説する。
まずコードを書き、次にテストを書き、そしてコードが間違っていたことに気づく。これが標準的なループだ。だからデバッグは、ほとんどのプロジェクトのタイムラインの半分を消費する。 Box…
IBM は開発者に自身のコード実行を禁止し、0.1 defects/KLOC のソフトウェアを出荷した
IBM の Cleanroom エンジニアリング・プロセスは、バグを発見するのではなく未然に防ぐことで、業界平均より 100 倍優れた defect 率を達成した。それがどう機能したか、なぜほとんど誰も使わないのか、そして今日あなたが取り入れられるものとは。
IBM は NASA の衛星制御システムを KLOC あたり 0.1 欠陥という水準で出荷した。当時の業界平均は 10 から 50 の間だった。彼らがこれを達成したのは、より優秀な技術者を採用したり、より長時間働いたりしたからではない。開発者に自身のコードを実行することを禁じたからだ。 これが Cleanroom…
CI があなたなしで tangle できない限り、あなたのリテラート・プログラムは壊れている
Literate programming は単一事実情報源を約束するが、手動の weave と tangle のステップが CI/CD パイプラインを破壊する。Markdown ファイルを正規のものに保つため、抽出とドキュメント生成を自動化する方法を紹介する。
ビルドパイプラインが、ターミナルを開いて と打たなければ実行できないなら、あなたはリテラート・プログラムを持っていない。コンパイラの付いた日記を持っているだけだ。 リテラート・プログラミングの全目的は、散文とコードが単一事実情報源を共有することにある。Markdown…
コードを先にLLMに説明したら、バグ率が85%減少した
30日間、LLMにコードを依頼する前に設計の説明を書き続けた。その結果は、私のrubber-duckingに対する考え方を変えた。
ほとんどの開発者はLLMを逆さまに使っている。5語ほどで欲しいものを説明し、200行のコードを受け取り、次の1時間はモデルが行った仮定をデバッグすることに費やす。…
テスト、コード、散文を1つのMarkdownファイルにまとめて、ドキュメントへのコードコピーをやめた
Literate programmingは、Markdownファイルをsingle source of truthにすることで、ドキュメント、テスト、実装を同期させ続ける。Python30行で実装する方法を紹介する。
ドキュメント、テスト、コードは、同じことをまともに語れない3つのファイルだ。 ソースの関数シグネチャを更新する。READMEのサンプルを忘れる。1週間後、新入社員が古くなったスニペットを本番にコピーする。テストファイルはまだ古い動作を期待結果としてエンコードしている。これでバグが2つ、ドキュメントチケットが1つだ。…
あなたのClaudeスレッドはすでにドキュメントです。ただ、12時間で消えてしまうだけ。
LLMの対話には意図、却下された代替案、そして動作するコードが含まれています。これこそがドキュメントであるべきものです。以下に、短寿命なチャットをナラティブを失うことなく、永続的で検索可能なドキュメントに変換する方法を説明します。
あなたはClaudeと45分かけてリトライ回路を設計しました。失敗モードを説明し、カスケード圧力を隠してしまうため指数関数的バックオフを却下し、jitter付きtoken-bucket rate limitingで決着し、動作する実装を生成しました。説明は明快で、推論は妥当であり、コードは実際にテストをパスしました。…