Skip to content

backlog(B-0142): resurrect .NET Code Contracts in F#/dotnet 10 (Aaron 'maybe we could resurect' 2026-05-01)#1114

Closed
AceHack wants to merge 2 commits intomainfrom
backlog/B-0142-resurrect-dotnet-code-contracts-aaron-2026-05-01
Closed

backlog(B-0142): resurrect .NET Code Contracts in F#/dotnet 10 (Aaron 'maybe we could resurect' 2026-05-01)#1114
AceHack wants to merge 2 commits intomainfrom
backlog/B-0142-resurrect-dotnet-code-contracts-aaron-2026-05-01

Conversation

@AceHack
Copy link
Copy Markdown
Member

@AceHack AceHack commented May 1, 2026

Summary

P3 backlog row per Aaron's "me to you:" framing 2026-05-01 — speculative-research-class exploration of resurrecting Microsoft Research's Code Contracts library (died ~2017) in modern F# / dotnet 10.

Aaron's verbatim:

Design-by-contract used to be supported in dotnet first class Code Contracts. it died.

maybe we could resurect

they could not fgured out how to make to preformant

but the primitives are in the dotnet frameowr but noops

Search-first verification (per CLAUDE.md version-currency-always-search-first)

The System.Diagnostics.Contracts namespace + Contract.Requires / Contract.Ensures / Contract.Invariant primitives still exist as no-ops in modern .NET; the toolchain (rewriter ccrewrite + static verifier cccheck) was deprecated. Microsoft Learn confirms: "no Code Contract 'tooling' available in Visual Studio 2013 or in the latest versions of the .NET Framework" — but the open-source library remains on GitHub.

The historical reason for death: perf-overhead from contract-rewriter inserted runtime checks + static-verifier soundness/incompleteness/scaling issues.

Resurrection-path candidates

  • Source-generator-based compile-time injection (modern; zero runtime overhead in release)
  • Runtime-rewriter approach (closest to original; runtime overhead but more flexible)
  • Hybrid (compile-time invariants; runtime pre/post)

Acceptance criteria laid out

  1. Prior-art audit (Code Contracts / Eiffel / Spec# / Dafny / LiquidF# / Roslyn analyzers / F# computation expressions / Zen / FsCheck)
  2. Design proposal selecting toolchain shape
  3. Perf budget (load-bearing constraint that killed the original): <5% release-mode overhead vs non-contracted hot path
  4. F#-idiomatic syntax (not C# 1:1 port)
  5. Verification integration (feeds Soraya's TLA+/Lean/Z3/FsCheck portfolio)
  6. Composes with B-0141 (pre/post pattern as abstract class; DbC = concrete instantiation)

Composes with

Test plan

  • Frontmatter schema (B-0142 / P3 / open / 2026-05-01)
  • BACKLOG.md regenerated via BACKLOG_WRITE_FORCE=1 ./tools/backlog/generate-index.sh
  • Aaron's "me to you:" verbatim preserved
  • Search-first verification per version-currency rule
  • Sources cited

🤖 Generated with Claude Code

@AceHack @claude
backlog(B-0142): resurrect .NET Code Contracts in F#/dotnet 10 — desi…
9ec9035 
…gn-by-contract resurrection per Aaron 'maybe we could resurect' (2026-05-01)

Aaron's verbatim "me to you:" framing during the SRE / DbC
prior-art discussion (B-0141 follow-up):
- "Design-by-contract used to be supported in dotnet first
  class Code Contracts. it died."
- "maybe we could resurect"
- "they could not fgured out how to make to preformant"
- "but the primitives are in the dotnet frameowr but noops"

P3 (research-grade exploration; long-horizon; substantive
effort). Filing IS the action; implementation deferred.

Search-first verification 2026-05-01 (per
version-currency-always-search-first rule): the
System.Diagnostics.Contracts namespace + Contract.Requires/
Ensures/Invariant primitives still exist as no-ops in modern
.NET; the rewriter (ccrewrite) + static verifier (cccheck)
toolchain was deprecated. Microsoft Learn confirms: "no Code
Contract 'tooling' available in Visual Studio 2013 or in the
latest versions of the .NET Framework" but the open-source
library remains on GitHub.

Acceptance criteria laid out: prior-art audit (Code Contracts
+ Eiffel + Spec# + Dafny + LiquidF# + Roslyn analyzers + F#
computation expressions); design proposal (source-generator
vs runtime-rewriter vs hybrid); perf budget (<5% release-mode
overhead — the load-bearing constraint that killed the
original); F#-idiomatic syntax (not C# 1:1 port); verification
integration (feeds Soraya's TLA+/Lean/Z3/FsCheck portfolio).

Composes with B-0141 (pre/post pattern as the abstract
architectural class — DbC is one concrete instantiation).

Sources cited per search-first authority rule.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Copilot AI review requested due to automatic review settings May 1, 2026 12:57
Copilot AI reviewed May 1, 2026
View reviewed changes
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

Adds a new P3 backlog row proposing a research-grade exploration of resurrecting/modernizing .NET Code Contracts for Zeta’s F#/.NET 10 stack, and updates the generated backlog index to include it.

Changes:

  • Added new backlog row B-0142 documenting motivation, candidate approaches, acceptance criteria, and sources.
  • Regenerated/updated docs/BACKLOG.md to include the new B-0142 entry.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File Description
docs/backlog/P3/B-0142-resurrect-dotnet-code-contracts-aaron-2026-05-01.md New P3 backlog entry describing a Code Contracts resurrection investigation with acceptance criteria and citations.
docs/BACKLOG.md Adds B-0142 to the auto-generated backlog index.

Comment thread docs/backlog/P3/B-0142-resurrect-dotnet-code-contracts-aaron-2026-05-01.md Outdated
Comment thread docs/backlog/P3/B-0142-resurrect-dotnet-code-contracts-aaron-2026-05-01.md Outdated
Comment thread docs/backlog/P3/B-0142-resurrect-dotnet-code-contracts-aaron-2026-05-01.md Outdated
@AceHack
fix(B-0142): markdownlint MD049 + grammar + dangling refs (Copilot P1…
5f11e16 
…/P2 + lint)

- Line 58 (P2 grammar): "could not figured out" → "could not
  figure out" (paraphrase grammar-correction marked).
- Line 111 (P1 xref): glob `feedback_pirate_not_priest_*` →
  full path `memory/feedback_aaron_pirate_not_priest_*.md`.
- Line 172 (P1 xref): "CLAUDE.md § Claude-Code-harness"
  framing wrong (CLAUDE.md doesn't section-number) → quoted
  actual heading + bullet name.
- Line 174 (markdownlint MD049): `Result<_,_>` was parsed as
  emphasis (underscore vs asterisk style); wrapped in
  backticks so it renders as code-span.
@AceHack AceHack enabled auto-merge (squash) May 1, 2026 23:51
@AceHack
Copy link
Copy Markdown
Member Author

AceHack commented May 3, 2026

Superseded by merged #1349 (B-0142 Code Contracts revival) — main has the row file at docs/backlog/P2/B-0142-code-contracts-design-by-contract-revival-aaron-2026-05-01.md. Content from this PR not carried into the merged version: perf budget (<5% release-mode overhead, the load-bearing constraint that killed the original); prior-art audit (Code Contracts / Eiffel / Spec# / Dafny / LiquidF# / Roslyn analyzers / F# computation expressions / Zen / FsCheck); source-generator-based compile-time injection vs runtime-rewriter vs hybrid candidates; F#-idiomatic-syntax constraint; composes-with-Soraya's-verifier-portfolio integration; LiquidF# Day-0 Hold reference. Available in this PR's git history (commit 9ec9035076f2ae8abb25ed310ba66c5d2e2b5259) for future-Otto / future-implementation reference. Closing as superseded per Aaron 2026-05-03 authorization.

@AceHack AceHack closed this May 3, 2026
auto-merge was automatically disabled May 3, 2026 08:37

Pull request was closed

@AceHack AceHack mentioned this pull request May 3, 2026
Merged
3 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot Copilot left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@AceHack