Skip to main content

2 posts tagged with "design"

View All Tags

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

· 9 min read
axe
Creator of Ora

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?

Introducing Ora's Type System: Zig Meets Rust on the EVM

· 6 min read
axe
Creator of Ora

Smart contracts need a type system that's both safe and predictable. After years of working with Solidity's implicit behaviors and Rust's complex ownership rules, we asked: what if we took the best parts of both and built something specifically for the EVM?

That's how Ora's type system came to be. It's Zig-first in philosophy (explicit, no hidden control flow), Rust-influenced in safety (affine types for resources), and EVM-native in execution (every construct maps clearly to bytecode).