oo-python-to-rust

Companion repo for the Coursera course Object-Oriented Programming: Python to Rust. The four pillars retargeted as provable contracts. Classical patterns + Rust-specific patterns + ADTs, each gated by YAML.

---

What this repo demonstrates

Rust doesn't have classes. The four OO pillars (encapsulation, substitutability, composition, polymorphism) are retargeted as provable contracts, then exercised across classical GoF patterns (Strategy, Decorator, Adapter), Rust-specific patterns (Newtype, session-type Builder), and the ADT-vs-trait alternative (the expression problem).

Every pattern is gated by a YAML contract. The contracts are checked by pv (schema + score), pmat comply (coverage), proptest (behavioural), static_assertions (layout), and Lean 4 (formal). Coverage gate is 100% on cargo llvm-cov.

Examples

Domain throughout is UFC + BJJ: BeltStripes(max=4) for the encapsulation invariant, three Coach impls (HardcoreCoach / ChillCoach / StrategicCoach) for substitutability, Promotion composing FightCard + CornerNotes for composition-over-inheritance, Matchmaking Strategy + LoggingCoach Decorator + PromoterAdapter for the classical GoF patterns, FighterId newtype + Builder<FightBooking> typestate for the Rust-specific patterns, FightWin ADT (Knockout / Submission / Decision) for the expression problem, and the Cornerman hierarchy (HeadCoach / StrikingCoach / GrapplingCoach) for the capstone refactor.

Quick start

make install          # pv + pmat on PATH
make comply-init      # one-time: writes .pmat/project.toml
make ci               # fmt + clippy + test + coverage (100%) + pv lint + pmat comply

The ten contracts

Contract	What it asserts
oo-encapsulation-v1	Invariant fields are private; methods preserve invariants
oo-trait-substitutability-v1	All impls of a trait are behaviourally substitutable (Liskov)
oo-composition-over-inheritance-v1	No method-forwarding parent fields; shared behaviour via traits
oo-static-dispatch-zero-cost-v1	Monomorphized generic asm = hand-inlined asm
oo-object-safety-v1	dyn-traits satisfy object-safety; Vec<Box<dyn T>> typechecks
oo-newtype-zero-overhead-v1	repr(transparent) newtype has identical size + align + ABI
oo-strategy-v1	Strategy = trait + ≥ 3 substitutable impls + consistent dispatch
oo-decorator-delegation-v1	Wrapper preserves documented properties; single delegation per method
oo-adapter-compatibility-v1	Adapter round-trips T ↔ L; L does not impl T directly
oo-session-type-v1	Phantom-state typestate rejects illegal transitions at compile time

Module map

Module	Crate	Theme
M1	m1-pillars	The four pillars as contract bundles
M2	m2-classical	Strategy, Decorator, Adapter (substitutability + delegation + round-trip)
M3	m3-rust-specific	Newtype (layout) + session-type Builder (typestate)
M4	m4-adt-vs-traits	The expression problem; ADTs as the closed-set alternative
M5	m5-capstone	Refactor a Python class hierarchy + author the proof bundle

Python companion notebooks

One testable notebook per module. Every code cell ends in assert statements; make notebooks-test executes each top-to-bottom and fails the build if any assertion fires. Lint + format via ruff (configured in pyproject.toml); env via uv.

Module	Notebook	Open in Colab
M1 — Four Pillars	notebooks/m1-pillars.ipynb
M2 — Strategy / Decorator / Adapter	notebooks/m2-classical.ipynb
M3 — Newtype + Session-type Builder	notebooks/m3-rust-specific.ipynb
M4 — ADT vs Trait	notebooks/m4-adt-vs-traits.ipynb
M5 — Capstone: Notifier hierarchy	notebooks/m5-capstone.ipynb

The notebook source of truth is scripts/build_notebooks.py. Regenerate via make notebooks-build; verify everything via make notebooks-ci (build + format-check + lint + execute).

Methodology

Per the PAIML Provable Contracts methodology: never write code without a contract. Every pub item in this workspace is bound to at least one contract via contracts/binding.yaml, and pmat comply check blocks the build if a binding is missing.

The course this repo accompanies is the final design-and-modeling course in a 31-course Rust specialization, taken after c7 Design by Provable Contracts and big-o-python-to-rust. Familiarity with pv, proptest, and static_assertions is assumed.

License

Dual-licensed under MIT and Apache 2.0.