Contract-oriented language notes

This is a reference sketch for a possible kit-hosted language centered on design by contract, local reasoning, explicit effects, and typed communication. It is not a plan of record. The purpose is to preserve the design influences and the lessons worth carrying forward before any syntax or implementation work starts.

Goal

The language should make module boundaries unusually clear:

• Interfaces state types, contracts, effects, and communication protocols.
• Implementations hide representation and authority.
• Effects are explicit and mockable through interpreters or capabilities.
• Stateful protocols are expressed with typed channels/session endpoints.
• Modules can be implemented and tested in parallel against stable interfaces.
• Local reasoning is the default user experience; formal proof is optional, not the entry cost.

The design should favor ordinary modular engineering over proof theater. Stronger static checking is useful where it improves separation and confidence, but the first-class user story is "I can read this interface and know what clients and implementations owe each other."

Influence map

Area	Languages / systems	Lesson
Design by contract	Eiffel, D contracts, Racket contracts, Spec#, JML, ACSL	Put preconditions, postconditions, invariants, and blame at boundaries. Keep contracts executable before requiring proof.
Safety-critical modularity	Ada, SPARK	Package specs/bodies are a strong model for interface/implementation separation. SPARK's flow/contracts/proof model is valuable, but the language should not require proof culture for normal use.
Module systems	SML, OCaml, Modula-2/3, Mesa, CLU	Signatures, opaque types, and functors are the best precedent for decoupled modules, parallel implementation, and trivial substitution in tests.
Local reasoning and authority	Rust, Cyclone, Clean, ATS, Pony	Ownership, borrowing, uniqueness, and reference capabilities are useful for bounding aliasing and mutation. Use the parts that keep authority visible without making all code annotation-heavy.
Algebraic effects	Koka, Effekt, Frank, Unison, OCaml 5 research	Effects belong in computation types and should be handled by ordinary user-defined interpreters. Effect polymorphism is mandatory for ergonomics.
Capability security	E, Joe-E, Pony, object-capability systems	Authority should be passed explicitly. If a function cannot reach a capability, it cannot use it. Confinement is mostly about reference flow.
Channels and processes	CSP, occam, Newsqueak, Alef, Limbo, Go, Concurrent ML	Channels are a useful primitive, but untyped channel protocols drift into comments. CML-style composable events are worth studying.
Session types	Scribble, Links, Session C, Linear Haskell libraries	Protocol state should be part of endpoint types: send, receive, choose, offer, and close advance the channel state.
Coroutine state machines	C# async, Rust async/generators, Kotlin coroutines	Coroutines lower to state machines. The source language should make protocol state visible where useful while keeping generated state-machine plumbing opaque.
Actors and supervision	Erlang, Elixir, Pony, Orleans	Isolation and supervision are valuable. Untyped mailboxes are not enough for local reasoning; prefer typed endpoints/protocols.
Mocking and dependency substitution	ML functors, Go interfaces, Rust traits, Swift protocols, Haskell typeclasses	Testability comes from depending on narrow interfaces or capabilities, not globals. ML functors and effect handlers are especially clean substitution mechanisms.

Main takeaways

Eiffel gives vocabulary, not the whole shape

Eiffel's require, ensure, and invariants are the obvious design-by-contract reference. The useful part is the vocabulary and the idea that contracts are part of the callable interface. The less useful part is tying contracts deeply to inheritance. Contract inheritance gets subtle, and runtime-only contracts do not give enough modular leverage by themselves.

Carry forward:

• Preconditions on callers.
• Postconditions on implementers.
• Type and module invariants.
• old(...) values in postconditions.
• Runtime checking as the first implementation path.

Avoid:

• Making inheritance the main reuse or contract mechanism.
• Treating contracts as comments.
• Requiring whole-program verification before contracts are useful.

Ada/SPARK is the best systems-language precedent

Ada's package spec/body split maps directly onto the desired separation between interface and implementation. SPARK adds contracts, flow analysis, absence of runtime errors, and proof-oriented tooling. It is a strong influence for module discipline even if this language starts with lighter-weight checks.

Carry forward:

• Explicit package/module interfaces.
• Separate implementation bodies.
• Contracts attached to specs.
• Optional ghost/spec-only code.
• Flow/effect summaries that help readers understand dependencies.

Avoid:

• Making the proof subset feel like a separate language too early.
• Letting annotation burden dominate normal code.

SML/OCaml should heavily influence modules

SML signatures and functors are probably the strongest direct model for the module layer:

• A signature says what a module provides.
• The implementation can hide representation behind opaque types.
• A functor parameterizes one module over another.
• Tests and mocks are just alternate modules satisfying the same signature.

This is a better foundation for parallel implementation than inheritance or ambient dependency injection.

Effects should track computation, not object reachability

The important ergonomic rule from Koka, Effekt, Unison, Haskell, and related systems is that effects are attached to computations, not to mere possession of values.

A function should not become uses IO just because it accepts a struct that transitively contains an I/O capability. Passing, storing, comparing, or reading ordinary fields of that struct can still be pure. The effect appears when the function invokes an operation that uses the capability, delegates it, or leaks it in a way the type system cares about.

Distinguish three facts:

• Possession: a value contains or can reach authority.
• Use: a computation performs an operation through that authority.
• Escape: a computation stores, returns, sends, captures, or delegates that authority.

Most ergonomic systems track use by default. Security-sensitive systems also track escape.

Go channels are a warning, not the target

Go shows that channels can be pleasant, but untyped protocols do not preserve local reasoning. A chan Msg says little about the legal sequence of messages. For protocol-heavy code, the type should describe the session:

• Which side sends first.
• What choices are available.
• Which state follows each message.
• When the endpoint is closed.

Session types are the right reference. Go-like syntax may be ergonomic, but the semantics should be closer to typed protocol endpoints.

Coroutines need typed cancellation and cleanup

Coroutine state machines interact with resources and channels. The design needs explicit answers for:

• Cancellation propagation.
• Cleanup/finalization of linear resources.
• Protocol closure on early return.
• Which effects may suspend.
• Whether handlers can resume once, many times, or not at all.

These are interface concerns, not runtime afterthoughts.

Effects, capabilities, and data structures

The central ergonomic problem:

If a struct contains a capability, must every function accepting that struct be marked with the capability's effect?

The answer should be no.

Effects should track what the computation can do through the operations it actually performs, not every authority reachable inside every value it receives.

For example:

struct Server {
  cfg: Config,
  log: Logger,
  store: Store,
  metrics: Metrics
}

This should be pure:

fn server_name(s: Server) -> String
{
  s.cfg.name
}

This should carry effects because it invokes effectful operations:

fn handle(s: Server, req: Request) -> Response
  uses { Log, Store }
{
  s.log.info("request")
  s.store.get(req.key)
}

The type system should not punish coarse-grained structs by marking every consumer effectful. Instead, it should encourage narrower views when a function only needs part of a value:

interface HasConfig {
  fn config(self) -> Config
}

interface HasStore {
  fn get(self, key: Key) -> Value? uses Store
}

Authority facts worth separating

The language may eventually want separate summaries for different authority flows:

uses     { Store }  // may perform Store operations during this call
captures { Store } // may retain Store authority after this call
returns  { Store } // may return Store authority to the caller
sends    { Store } // may transfer Store authority over a channel

Only uses needs to be in the first design. The others are useful concepts for security-critical modules, plugin sandboxes, and confinement checks.

Recommended default rule

Default effect checking:

• Passing a capability-bearing value is pure.
• Loading a pure field is pure.
• Calling an operation with uses E gives the caller uses E.
• Calling a generic callback inherits the callback's effects.
• Returning or storing a capability is not a use effect, but may be checked by a stricter authority-flow mode.
• Sending a capability over a channel is a delegation event, not just ordinary I/O.

That keeps ordinary code ergonomic while leaving room for stricter boundary audits.

Effect polymorphism is non-negotiable

Without effect polymorphism, every higher-order helper becomes either unusable or over-annotated.

fn map<A, B, e>(xs: List<A>, f: fn(A) -> B uses e) -> List<B>
  uses e

The same applies to resource helpers:

fn with_lock<T, e>(m: Mutex, body: fn() -> T uses e) -> T
  uses e

The helper should add only its own effects. It should not erase or manually restate the callback's effects.

Capability narrowing is the main ergonomic tool

Large environment structs are useful at composition roots, but most functions should depend on narrow capabilities:

interface Clock {
  fn now(self) -> Instant uses Clock
}

interface Logger {
  fn info(self, msg: String) -> Unit uses Log
}

interface Store<K, V> {
  fn get(self, key: K) -> V? uses Store
  fn put(self, key: K, value: V) -> Unit uses Store
}

Tests replace these interfaces with in-memory interpreters. Production passes real interpreters. No global patching is needed.

Contracts

Contracts should live in interfaces whenever they describe client-visible behavior:

interface AccountStore {
  abstract Account

  fn transfer(src: Account, dst: Account, amount: Money) -> Unit
    requires amount > 0
    requires balance(src) >= amount
    ensures balance(src) == old(balance(src)) - amount
    ensures balance(dst) == old(balance(dst)) + amount
    uses { Store }
}

Implementation-private contracts are still useful, but they should not be the only place where behavior is specified. The caller should not need to read the implementation to know the obligations.

Contract levels

Useful levels, from cheapest to strongest:

• Documentation-level contracts: parsed and attached to symbols, even before checking.
• Runtime contracts: checked at debug/test boundaries.
• Static local checks: obvious precondition discharge, exhaustiveness, initialization, protocol state, purity.
• Optional proof: ghost values, lemmas, solver integration, or external tools.

The language should start by making the first two pleasant and preserving a path to the latter two.

Blame matters

Racket's contract system is worth studying because it assigns blame across module boundaries. When a precondition fails, the caller is wrong. When a postcondition fails, the implementation is wrong. This is important for parallel module work: failures should point to the side that broke the interface.

Modules

A module interface should be the main unit of decoupling:

module interface Store {
  abstract Key
  abstract Value

  effect Store

  fn get(k: Key) -> Value? uses Store
  fn put(k: Key, v: Value) -> Unit uses Store
}

An implementation supplies representation and an interpreter:

module MemoryStore : Store {
  type Key = String
  type Value = Bytes

  struct State { map: Map<String, Bytes> }

  fn get(k: Key) -> Value? uses Store { ... }
  fn put(k: Key, v: Value) -> Unit uses Store { ... }
}

The implementation may store capabilities internally, but clients can only use the authority exposed by the interface.

Desirable module properties

• Private by default.
• Explicit exports.
• Opaque types by default across interfaces.
• Ability to reveal type equality selectively.
• Parameterized modules/functors for dependency injection.
• Interface-level contracts and effects.
• Separate compilation against signatures.
• Mock modules that satisfy the same signature as production modules.

Effects and handlers

There are two related but distinct implementation models:

• Capabilities as explicit values with effectful methods.
• Algebraic effects as named operations handled by interpreters.

The surface can support both if the interface model is disciplined. A capability object is often the ergonomic value passed around; the operation it performs is what contributes to the effect row.

effect Log {
  op info(msg: String) -> Unit
  op warn(msg: String) -> Unit
}

handler MemoryLog : Log {
  ...
}

Mocking then becomes ordinary interpretation:

test "logs request id" {
  let log = MemoryLog.new()
  let store = MemoryStore.new()
  handle(log, store, req)
  assert log.contains("request")
}

No ambient global logger is required.

Channels and session types

Channels should carry protocols, not just payload types.

protocol StoreSession<K, V> =
  loop {
    choice {
      Get(K) -> recv V? -> continue
      Put(K, V) -> recv Ack -> continue
      Close -> end
    }
  }

The exact syntax is not important yet. The important semantic property is that using an endpoint advances its type:

let ch1 = send ch0, Get(key)
let (ch2, value) = recv ch1

This is the core local reasoning rule: after a send, the old endpoint state is gone. The program cannot send the wrong next message because the endpoint no longer has that type.

Structs containing endpoints

Storing endpoints in structs should be allowed, but use must respect linear or affine state:

struct Client<P> {
  endpoint: Endpoint<P>
}

Operations that advance the endpoint must also advance the containing value's state, borrow the endpoint linearly, or return an updated client:

fn get<K, V, P>(c: Client<P>, key: K) -> (Client<P>, V?)
  where P supports StoreSession<K, V>

The exact mechanics are open. The invariant is not: an endpoint cannot be used twice at the same protocol state.

Local reasoning rules

A reader should be able to inspect a function signature and know:

• Which abstract types and interfaces it depends on.
• Which contracts callers must satisfy.
• Which contracts implementations promise.
• Which effects it may perform.
• Which capabilities it may retain or delegate, when stricter mode is enabled.
• Which channel protocols it may advance.
• Which state is mutable and who can alias it.

This implies a few likely defaults:

• No hidden global state.
• No ambient I/O.
• Private representation by default.
• Explicit capability arguments or module parameters.
• Effects on operations, not on data possession.
• Linear or affine treatment for session endpoints.
• Runtime contracts enabled in tests/debug builds.

Design hazards

Avoid these traps:

• Transitive effect pollution. Marking every function that accepts a capability-bearing struct as effectful makes the system unusable.
• Untyped protocol comments. If a channel protocol lives in prose, it will drift.
• Proof-first ergonomics. Optional proof is useful; mandatory proof blocks adoption.
• Inheritance-centered contracts. Composition, modules, and interfaces fit the goal better.
• Implicit global handlers. They make tests and authority audits harder.
• One giant environment type. Useful at the top level, harmful when it leaks into every helper.
• Effect rows without polymorphism. Annotation burden will explode.
• Session types without cleanup rules. Cancellation and early return must close or transfer endpoints predictably.

Likely starting point

A first cut should probably be small:

1. Module interfaces with abstract types.
2. Runtime-checked preconditions, postconditions, and invariants.
3. Explicit capability values and narrow interfaces.
4. Computation-level effect summaries with effect polymorphism.
5. Opaque implementation bodies.
6. Basic typed channels.
7. Session typing once linear/affine endpoint ownership is designed.

The first implementation does not need a theorem prover, full algebraic effects, or complete session typing. It should establish the boundary discipline: interfaces are where contracts, authority, and protocols are declared; bodies are where representations and interpreters live.