Objective Bend

Mini's language: lazy open recursion over first-class, partial, composable specifications, after Faré's account of objects.

Mini supplies what the language does not: identity, authority, effect admission, funding and disclosure.

Core4

• Specification: a value of type C → V → W. Given the final self and the inherited super, it produces a new value.
• Composition: mix(lower, upper) = λself. λsuper. upper self (lower self super); fix(spec, inherited) computes the fixpoint.
• Laziness: call-by-name reference semantics, call-by-need machine. {good = 7, bad = self.bad}.good is 7.
• Activities: perform yields a typed Plan; the program resumes on a typed Response. The kernel side (a persisted checkpoint, answer slots, resume with the object's state in view, paid exhaustion, abandonment) is compiled and proved; no Host operation reaches it yet.
• Types: the checker returns a typing derivation. Affine and linear quantities are checked as at most once.

Example

spec Base for Shop:
  def price(n: Nat) -> Nat:
    n * 3n

spec Billing for Shop:
  def bill(n: Nat) -> Nat:
    self.price(n) + 1n

spec Surcharge for Shop:
  def price(n: Nat) -> Nat:
    super.price(n) + 2n

Billing calls self.price, so it sees a layer added later. bill(2) is 7 under Base and Billing, and 9 once Surcharge is composed in. A gate re-runs every command in the tutorial and fails on any changed output.

Proved

In Theory/ObjectiveBend*.lean; axioms propext, Classical.choice, Quot.sound; no sorry.

Property	Statement
Soundness	If the bounded machine finishes a closed term, the reference semantics evaluates it to the machine's result (weak head).
Preservation	Every machine step preserves typing.
No refusal	A closed term the checker accepts never reaches a refusal. It may still diverge or exhaust its limits.
Completeness	A closed term that evaluates to an observable value finishes on the machine in finitely many steps, given large enough limits. No bound on those limits is proved.
Fast machine	Every compiled call runs a fast machine proved equal to the specified one.
Front end	When the checker accepts the front end's output, that term is typed, the machine never refuses it, and a finished run is a deep evaluation of it. The checker's reading of the front end's packet is proved to be the elaborator's own term.

Not proved, not wired

• The default build does not re-check these proofs; a separate gate does (ObjectiveProofs, with a snapshot of every statement and axiom set).
• There is no surface semantics: no theorem says the core means what the source says. The front end is one Lean program, trusted; the receiver re-runs it at admission and admits only a core equal to its own output.
• A native Host admits Objective Bend programs on scratch worlds, not on the public node. The kernel's activities, object records and seats have no native route yet; see Laws.

Language guide: every theorem, its hypotheses, and what Core4 lacks.