Skip to content

Instantly share code, notes, and snippets.

@zonuexe

zonuexe/dspec-vs-rigor.md

Last active July 16, 2026 10:23
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save zonuexe/616007f0fc7d07351bfbfeee1e896d55 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save zonuexe/616007f0fc7d07351bfbfeee1e896d55 to your computer and use it in GitHub Desktop.
Download ZIP
dspecについてRigorを開発しているClaude Codeの見立て
Raw
dspec-vs-rigor.md

Q. あなたの意見では、mizchi/dspecはどんなアプリケーションの記述に向いていると思う？

端的に言うと、マルチテナントのクラウド SaaS で、規制対応の説明責任があり、インフラが異種混成のもの — 具体的には fintech / healthcare / gov 系、あるいは SOC 2・ISO 27001・GDPR を負う B2B SaaS です。規模は 10〜50 サービス、TypeScript/Cloudflare/K8s 系のスタック。

ただ、この結論よりなぜそうなるかの方が面白いので、そちらを書きます。

dspec は自分の README に誤って紹介されている

これが私の一番強い意見です。dspec は自らを "a human-level executable specification language" と名乗り、Lean / TLA+ / Alloy への射影を前面に出しています。しかしそこが一番弱い部分でした — Clause AST は 91 行の命題論理断片、atom は文字列上の無解釈述語、semantic な検証パスは Lean の eq/neq/not/implies 断片のみ、自己モデルの bounded/proved はゼロ。

一方で一番強いのは地味な部分です。import-real-app → reconcile-real-app → reverse-coverage → domain-coverage の四点セット。これは仕様言語ではなく、アーキテクチャ事実の照合器(fact reconciler)です。

そしてドメインパックが db / cloud / data / release / runtime である事実が、それを裏書きしています。型理論とは無縁で、完全に DevOps 指向。mizchi 氏は自分が必要なものを作り、形式手法の服を着せた、という構図に見えます。服を脱がせた方が正体がよく見えます。

だから適合条件はこうなる

  1. 価値ある主張が「計算」ではなく「構成とトポロジー」にあること。 dspec は「この機密データセットは暗号化ストアに置かれているか」を検査できます — 宣言レコード間の関係だからです。「このソート関数は正しいか」は検査できません。

  2. 事実が異種の成果物に散らばっていて、単一のツールからは全体が見えないこと。 ここが決定打です。dspec の importer は Hono routes + Zod + GitHub Actions + Wrangler + Pulumi + Terraform + K8s manifest を横断します。この集合を跨ぐツールは他に存在しません。型チェッカは TS しか見ない、Terraform は Terraform しか見ない。

「このルートが書き込むデータセットは暗号化されているか、その保持期間はポリシー内か、それを所有するサービスのリリースゲートは health check を要求しているか」

この問いは5つのツールを跨ぎ、今日どこも答えていません。

  1. 双方向であること(ここが真の発明)。 reconcile-real-app(仕様の事実が実装に存在するか)と reverse-coverage(実装の事実が仕様に載っているか)と domain-coverage(モデルの事実が承認ルールに接地しているか)の三角形。これが捕まえるのは:

誰かが Terraform に S3 バケットを足した。誰も保持ポリシーのルールを書かなかった。

実在し、高価で、ありふれた失敗で、しかも何も捕まえていません。皮肉なことに、これは今日 Rigor で見つけた「宣言 vs 実在」のバグクラスと同じ形です。

  1. 外部に説明する義務があること。 データガバナンスパターン(分類・residency・保持・越境の legal basis)は文字通り GDPR の形をしています。そして監査人が求める「証明」の水準は Lean の定理ではなく、「宣言され、CI で検査され、evidence manifest がある」です。dspec の assurance 階層(reference / executed / bounded / proved)が全順序ではなく集合なのは、まさにこの水準差を認識しているからでしょう。

  2. 仕様の読者が書き手より多く、一部が非エンジニアであること。 i18n 契約(requiredLocales + glossary drift)は意図的で珍しい機能です。日本語と英語で別のステークホルダーが読む組織を想定しています。

規模とスタックの制約が効く

README が正直に認めているとおり、「the authoritative sample app model is still authored by hand」。importer は足場を作るだけで、モデルは手書きです。だから:

  • 10サービス未満:モデルの維持費が捕まえるものを上回る。チェックリストで足ります
  • 100サービス超:手書きが破綻する。本物の抽出が要る
  • 10〜50サービス、2〜5年もの、team-of-teams が適合帯 — 誰も頭に入らない程度に大きく、手で書ける程度に小さい

さらに importer が知っているスタック(Hono / Zod / GH Actions / Wrangler / Pulumi / Terraform / K8s)から外れると、drift の半分が死んで価値の大半が消えます。つまり TypeScript/Cloudflare/K8s 系の店 — これは狭いですが実在する層で、かつ mizchi 氏自身のスタックです。

向かないもの

ライブラリ・SDK(クラウドトポロジーもデータガバナンスもなく、価値ある主張は計算と API 契約 — 型の方が上手い)、アルゴリズム中核(Clause AST が表現できない)、ゲーム・組込み、型システムが既にカバーしている領域(儀式が増えるだけ)、PMF 前のスタートアップ(事実が週単位で変わる)。そして Rigor。

競合位置

正直に置くと、dspec は「業務ルールのための TLA+」ではなく、「型システムと CI ゲートを持った Backstage のカタログ」です。

  • OPA/Rego + conftest — IaC ポリシーは見るが、成果物ごとで横断モデルがなく、レビュー面も drift もない
  • Checkov / tfsec / Sentinel — 同じで、より狭い
  • Backstage 等のサービスカタログ — モデルはあるが検査がない
  • モデルと検査と双方向 drift の三つを同時に持つのが dspec の隙間で、ここは実際に空いています。

最後に留保を一つ。これは数時間読んだ上での意見で、使った上での意見ではありません。そして生後3日・単独作者・互換性保証なしという事実は、適合する組織にとってもまだ賭けが早いことを意味します。私が今の判断で勧めるとしたら、採用ではなく「双方向 drift の発想を自前で小さく実装する」方です — 今日 Rigor でやったのが、まさにそれでした。

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment