Skip to main content

7 posts tagged with "compiler"

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?

Comptime in Ora: Compile-Time Work, Runtime Simplicity

· 6 min read
axe
Creator of Ora

Smart contracts live in a harsher environment than normal software: execution is expensive, everything is observable, and complexity becomes attack surface. "Good compilation" isn't just about speed—it's about predictability. Smaller runtime code. Fewer branches. Fewer guards. Less that can go wrong.

Ora's comptime pipeline exists to enforce that. When an expression is provably constant, the compiler evaluates it during compilation, replaces it with a literal, and lets the rest of the pipeline operate on something simpler than what the developer wrote.

That sounds obvious. In practice, it's one of the places where many smart-contract toolchains accumulate accidental complexity.

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).

Refinement Types: Making Smart Contracts Safer by Default

· 7 min read
axe
Creator of Ora

Smart contracts deal with money. That means every integer operation, every division, every transfer needs to be correct. Traditional type systems catch some bugs, but they don't catch the ones that actually matter: "is this value non-zero?", "is this amount above the minimum?", "is this rate within bounds?"

Refinement types fix that. They let you express constraints directly in the type system, and the compiler enforces them—at compile time when possible, at runtime when necessary.