One meaning, many projections.

A service is ordinary functions plus a contract.

Every service I have built had the same quiet failure: knowledge that belonged to the business ended up inside the machinery that moved the bytes. Serialization shapes in domain signatures. Error handling bent around one transport. Deployment facts in business packages. The advice to separate concerns is universal; what is missing is a mechanism that makes the separation checkable instead of aspirational. Koba is that mechanism. A service is a set of ordinary functions, written as if no network existed, plus a contract: a value that states what is true about their boundary regardless of how they are reached. Everything else is derived from that pair. The project began in 2021. Go is its first implementation, not its definition.

• The contract is a value registered beside the functions, never a method on them. It holds request bindings, rules, authorization and the failures a caller must handle.
• The core names no wire. HTTP, WebSocket, Kafka, gRPC and the others are libraries that implement one projection interface, and an in-process call is the identity projection.
• The plan, the OpenAPI document, the lock manifest and the documentation for people are derived from the same values that serve the requests, so none of them can drift from the service.

Four categories, one executor.

At registration a service states four things, each in its own category. The API is the functions. The contract is the boundary truth: typed rules, authorization scopes and declared outcomes. The wiring says which wires reach the service, and it lives at the composition root, not in the API. The deployment says how the contract’s dependencies are bound in each stage. Koba compiles the four into a normalized plan, and one executor runs every operation the same way, whatever wire built the invocation: authorize, invoke, validate, recover. A single placement rule decides where a fact belongs. It goes in the core if it holds regardless of wire, in a projection if changing it changes the wire, and in prose if it only changes what a person reads.

• Rules are values. A rule decides, supplies or annotates a possibly absent value and returns a judgement: a reason, not a verdict. The host type system checks where each one applies.
• A failure the caller must handle is a declared outcome with a typed payload. Once an operation declares its outcomes the set is closed, and an error outside it is a contract violation.
• Whether a value arrived, whether it is present and whether it may be null are three separate questions, answered the same way on every wire.
• Authorization is a closed scope algebra with three forms, has, every and some. It is monotone and has no negation.
• Effects are scoped computations, pure or IO, composed with bind, choice, bracket and scope, so the shape of a program is visible before it runs.

A decision or an accident?

A model with one implementation cannot tell the difference between a decision and an accident. So the Go implementation is not the oracle. The model is written down as a specification and built again in other languages, and the implementations run the same fixtures. When two of them disagree, a third shows which one held the accident. The Go implementation is validated and serves real applications. The specification is not yet implementable on its own, and what it lacks is counted and recorded beside it.

• Specification: four independent attempts to implement from the text and its fixtures alone, without reading the Go, found 40 blocking gaps, 61 places where two implementations would silently differ and 6 of wording.
• Java: compiled probes, a comparison against the shared fixtures and a register of the gaps between Koba and a second implementation. Domain types carry no annotations and no framework imports.
• Python: a base implementation with an in-process projection, an HTTP wire and a queue wire, and a third runner for the shared fixtures.
• TypeScript: an independent implementation with its own HTTP, WebSocket and rules modules, and a whole application built on them whose domain imports nothing from the framework.
• Comparing Go, Java and Python found three defects: one in the Go core, one in a shared fixture and one in the Java runner.

Toward an algebra of systems.

The aim is a precise way to compose independently developed concerns and say which guarantees a composition preserves. The working foundation exists: native functions, explicit contracts, composable execution. The algebra itself, the composition operations, their laws and an implementation-independent intermediate representation, is a direction, not a claim that it is already formalized. Three extensions of the model are specified but not built. A survey of 57 sources in seven families confirms that every piece has precedent; what remains to investigate is Koba’s particular integration.

• Workflows: a program whose life outlives an exchange, a connection and a process. Identity, suspension, replay and recovery are specified before any code is written.
• Provisioning: the resources, accounts and rights a service needs are inferred from its declaration, so the language is the code and the manifest is its intermediate representation.
• Capability admission: a workload runs only with evidence that the policies derived from its declared requirements are enforced, and stops if that evidence is lost.

Haskell on the go.

Kopo carries the same question at the language level: what is a program once its implementation is taken away? It is a lazy, typed, general-purpose functional language implemented and hosted in Go. Its starting point is Haskell’s semantics, not only its appearance: call-by-need evaluation, type inference, algebraic data types, pattern matching, typeclasses and effects as values. Go supplies the other half: a portable runtime, a practical toolchain, versioned modules and an explicit boundary to native code. Kopo is not a transpiler to Go, and GHC is a differential oracle for the shared subset, not the authority that defines the language. It already runs real programs; its syntax, ABI and standard library may still change.

• Semantic fidelity is measured, not asserted. Types, values, partiality, demand, sharing and productivity are compared against GHC for the shared subset. An implementation that produces the same value but forces it too early is not compatible.
• Interop with Go is honest. A Kopo list is not a Go slice, views across the boundary are explicit, and the purity of an imported Go function is an assertion made by the author of its binding.
• A program reaches only the capabilities its host binds.

Meaning, execution and access stay apart.

Parser combinators produce a surface syntax tree. Inference elaborates it into Core, a typed immutable intermediate representation, and Core is the only executable representation. A call-by-need machine written in Go runs it today; Core leaves room for other evaluators, and a bytecode machine is the planned second one. Three questions are kept apart on purpose: what a program means, how it is executed and what it can access. Compatibility with a useful core of Haskell is a tested profile, KHCP-1, with Haskell 2010 as its reference, and every semantic decision has a numbered record.

• Works today: type inference with prenex polymorphism, algebraic data types, records and patterns, single-parameter typeclasses with deriving, a Haskell-like Prelude, modules distributed through Go’s module system, a typed Go FFI, check, run, build to a self-contained executable, a transactional REPL and a language server.
• Not yet: rank-n types, GADTs, type families, multi-parameter classes, STM and a parallel runtime.

Requirements as types, admission before execution.

The thread I care most about is how a program states what it needs from its host without the host leaking into its meaning. A binding carries a row of requirements beside its type. A policy narrows what an entry point may use. The host presents evidence of what it provides. A plan is admitted only when semantics, host support, requirements and policy agree, and cost ranks only the plans that are already valid. Today this is a flat row per top-level binding and an admission step before a module initializes. The next step is requirements on function arrows, so that higher-order code carries them, and a calculus with a soundness argument before any novelty is claimed. Alongside it: self-hosting measured as which behavior is owned by Kopo source rather than by Go, and an experiment register where every entry states what would falsify it.

Kopo behind Koba operations.

In this design, Koba describes and exposes an operation whose business logic is written in Kopo. The operation stays application-owned and the transports stay projections. The purpose is explicit guarantees inside the business logic: typed domain values, contextual requirements that compose, and possibly more precise effect or resource profiles. Three integration depths are under study, and adoption should be possible per operation rather than by rewriting a service. Neither project depends on the other.