commit 6d73c1e5ebb79e9c76814b37342f5bdae0b96626
parent 977cc8c48aacd19bd104c05e46851cd5724acce5
Author: Ryan Sepassi <rsepassi@gmail.com>
Date: Mon, 13 Jul 2026 10:26:46 -0700
Document contract language design influences
Diffstat:
2 files changed, 508 insertions(+), 0 deletions(-)
diff --git a/doc/ideas/CONTRACT_LANG.md b/doc/ideas/CONTRACT_LANG.md
@@ -0,0 +1,507 @@
+# 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:
+
+```text
+struct Server {
+ cfg: Config,
+ log: Logger,
+ store: Store,
+ metrics: Metrics
+}
+```
+
+This should be pure:
+
+```text
+fn server_name(s: Server) -> String
+{
+ s.cfg.name
+}
+```
+
+This should carry effects because it invokes effectful operations:
+
+```text
+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:
+
+```text
+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:
+
+```text
+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.
+
+```text
+fn map<A, B, e>(xs: List<A>, f: fn(A) -> B uses e) -> List<B>
+ uses e
+```
+
+The same applies to resource helpers:
+
+```text
+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:
+
+```text
+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:
+
+```text
+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:
+
+```text
+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:
+
+```text
+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.
+
+```text
+effect Log {
+ op info(msg: String) -> Unit
+ op warn(msg: String) -> Unit
+}
+
+handler MemoryLog : Log {
+ ...
+}
+```
+
+Mocking then becomes ordinary interpretation:
+
+```text
+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.
+
+```text
+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:
+
+```text
+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:
+
+```text
+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:
+
+```text
+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.
+
diff --git a/doc/ideas/README.md b/doc/ideas/README.md
@@ -7,5 +7,6 @@ captured idea, not a plan of record.
| Sketch | Scope |
|--------|-------|
+| [CONTRACT_LANG.md](CONTRACT_LANG.md) | Notes for a possible contract-oriented language: design-by-contract influences, effect/capability ergonomics, modules, typed channels, and session-type lessons. |
| [RQL.md](RQL.md) | A typed relational query language (a clean-break SQL replacement): surface syntax, logical algebra/IR, physical plan, algebraic laws, option types instead of NULL. |
| [RSN.md](RSN.md) | A statically-typed scripting language to replace make/shell/Python for kit's build and test orchestration: typed CG-API frontend, staged arena/GC runtime, cooperative fibers. |
