Apparatus and Contraptions: A Two-Tier Approach to Type Design in a Verified Smart Contract Language

Designing types for smart contract languages has unusually high stakes. Types leak into ABI boundaries. Storage layouts become long-lived commitments. And small semantic choices can turn into permanent protocol constraints that survive long after the feature that introduced them has been forgotten. At the same time, the execution environment pushes us in the opposite direction. The EVM is a 256-bit stack machine with minimal native structure, and the most important operations in a contract—calls, state reads, state writes—carry both financial and adversarial weight. If you care about verification, those realities don't just influence the language. They define it.

Ora is a smart contract language and compiler for the EVM with explicit region/effect semantics, refinement types, and an MLIR-based pipeline backed by SMT solving. As the language matures beyond its core type system (integers, booleans, addresses, maps, structs, enums, and error unions), we keep coming back to the same problem. How do you extend a type system without freezing the language too early?

In most general-purpose languages, "adding a type" is a local decision. In a smart contract language it's rarely local. A new type tends to imply an ABI shape, a storage representation, a set of invariants that users will assume, and a set of verification obligations the compiler will carry forever. Even if the feature is never used widely, it still becomes part of the language's conceptual gravity. That is why we treat type additions less like a backlog and more like a design discipline.

One way we've learned to keep the discipline without becoming slow is to separate type candidates into two tiers. We call them Apparatus and Contraptions. The names are lightweight, but the distinction is serious. It's about confidence. Apparatus are the things you can build with and trust. Contraptions are the things you can build on, experiment with, and potentially discard without regret. The split is not a roadmap. Apparatus does not mean "next," and Contraptions does not mean "eventually." The tiers measure semantic maturity and confidence, not prioritization. Some Apparatus items may be deferred for months for reasons that have nothing to do with correctness. Some Contraptions may remain experimental forever, and that is a healthy outcome. The whole point is to keep experimentation fast and commitment slow.

An Apparatus, in our internal language, is a type or family of types whose meaning is already well understood. There is precedent. The EVM lowering is direct and explainable. The runtime representation is predictable. Open questions are engineering questions—layout, ABI, code generation—not the harder question of what the abstraction really means once it interacts with reentrancy, storage, upgrades, and adversarial calls. Most importantly, an Apparatus composes with what Ora already commits to. Refinements, error unions, regions and effects, the verification model. Apparatus is what we are willing to write into the specification and defend long-term. If we later regret an Apparatus addition, it is not just an internal refactor. It can become an ecosystem burden.

A Contraption is different. A Contraption is something that might be valuable, but where the meaning is still shifting, or where the cost model depends on usage patterns we do not yet understand, or where adding it would force new compiler machinery whose boundaries are not yet clear. Contraptions are not rejected. They are held deliberately. They are where we allow ourselves to ask "what if?" without converting every promising idea into permanent debt. In practice, Contraptions show up as prototypes, libraries, compiler-recognized patterns, or narrow experiments. They live there until the design stops changing, or until we decide that the idea was useful as a thought experiment but not as a language feature. Both outcomes are wins. What matters is that the language remains agile while the spec remains conservative.

The interesting thing, though, is that the two-tier split is not the end of the process. It's the beginning of the part that actually improves design quality. When you evaluate experimental candidates one by one, each one looks like it needs its own feature. When you hold them together and examine them as a set, you start seeing repeated demands on the compiler. Several distinct-looking ideas end up wanting the same enforcement machinery. The design question shifts from "should we add this type?" to "should we add the mechanism that makes multiple type ideas cheap to express and safe to use?"

We saw this first with what you might call time-shaped values. On-chain systems are full of values that are not best understood as static numbers, but as numbers that evolve between snapshots. It might look like a timelock, where a value is inaccessible until a moment and then suddenly becomes usable. It might look like a streaming balance, where a value increases linearly with time. It might look like an accumulator, where value only increases and is periodically checkpointed. These ideas look different at the surface, but they share a deeper structure. Storage holds a snapshot plus parameters, and reads compute the present value as a function of elapsed time. That observation is not just aesthetic. It has teeth. Once you admit derived values, you need disciplined updates. You need "settle before mutate" patterns so that changing a rate cannot implicitly create or destroy value. You want pure reads that compute derived value without mutating storage, and explicit settlement operations that materialize the derived value when needed. The useful outcome here is not "add a dozen time-aware types." It's to define a defensible runtime representation, typically some form of (snapshot, params, last_updated), and to build compiler machinery that enforces settlement protocols. The derivation rule is not a function stored on chain. It's a compile-time known rule with concrete lowering.

Then we noticed another repeated demand. Phase ordering. Smart contracts are full of informal protocols. First commit, then reveal. First initialize, then open. First settle, then change rate. These sequences are often written down in documentation or implied by conventions, and then silently violated somewhere in the codebase under pressure. This is a perfect category of bug for a type system to delete. A typestate interpretation reframes it as compile-time structure. A value carries a state tag, the compiler tracks that state across control flow, and the set of permitted operations depends on the current state. A transition updates the state in a way the compiler can see. Whether the surface syntax looks like a general state machine or a specialized two-phase construct, the underlying mechanism is the same. Phase tracking enforced by restricting which operations are valid. The practical advantage is not elegance. It's that "invalid sequence" becomes a compile-time error instead of a post-deployment surprise.

Finally, we kept running into constraints that are really about accounting. Some rules are global invariants, the kind you want to state and prove with SMT. Total supply equals the sum of balances. A relationship between multiple storage locations always holds. But other rules are local conservation laws, where the net delta across a set of values within a region of code must be zero. Others are monotonicity constraints. This value never decreases. This counter never rolls back. This checkpoint only moves forward. These are all variations of the same desire: to restrict what patterns of writes are allowed. The compiler can enforce some of these structurally when it can see the relevant writes and model their deltas precisely. SMT can enforce broader relational properties when the structure is too global for simple tracking. In narrow cases, a runtime check may still be appropriate. What unifies the cluster is the shift from verification-as-assertion to verification-as-structure. The more we can structurally forbid invalid mutation patterns, the smaller the SMT surface becomes, and the more predictable runtime behavior is under adversarial composition.

At this point it's tempting to say "so the language reduces to three primitives." That's not the claim. The claim is about agility. If many experimental candidates repeatedly demand the same enforcement machinery, we should build the machinery first. Once it exists, "types" often become library wrappers, compiler-recognized patterns, or small well-scoped sugar. That reduces bespoke compiler complexity and reduces the risk of permanent design mistakes. It also makes experimentation cheaper. We can prototype multiple Contraptions against the same mechanisms and compare them on semantics and cost without hard-committing to a large surface area. Convergence doesn't force everything into one abstraction. It simply tells us where the leverage is.

Underneath the naming, the workflow is straightforward. A candidate is proposed, then classified by confidence. Apparatus items are the ones whose semantics are stable enough to commit. Contraptions are the ones with open semantic questions, unclear cost profiles, or missing compiler machinery. Contraptions are prototyped cheaply and evaluated on representative workloads. Over time, some stabilize and can be specified. Others remain useful as patterns. Others are discarded. The classification is not a promise. It is a way to keep experimentation fast and commitment slow. The convergence step is what keeps the process from turning into a backlog. Instead of treating each Contraption as a separate feature request, we look for repeated demands and prioritize shared mechanisms.

Ora's type system has to evolve under constraints that make premature commitment costly. The Apparatus/Contraptions split is one tool we use to move quickly without locking the language too early. Apparatus captures what we are willing to write into the specification with stable semantics and predictable representations. Contraptions create a safe place to explore and prototype without turning every promising idea into permanent debt. The deeper insight is that experimental ideas often converge. Many "new types" are really requests for a small number of reusable enforcement mechanisms. By prioritizing mechanisms over surface syntax, we can prototype more ideas with fewer permanent commitments, reduce bespoke compiler complexity, and keep verification tractable.

Ora is an open-source smart contract language and compiler for the EVM. If you're interested in language design under adversarial constraints, compiler architecture, or verified programming models, follow the project and join the discussion.