2 posts tagged with "ora"

v0.2 lands three things that matter together: a real algebraic-data-type surface (enum payloads, Result<T, E>, unified pattern matching), an SMT verifier that fails closed where it used to fail silently (--explain cores, vacuity detection, datatype encoding for products and error unions), and the first slice of a static-dispatch trait system (impl conformance, bounded generics, extern trait for ABI-correct external calls). Underneath them: bounded loop unrolling and ADT-aware comptime, an LSP that reflects the new surface, and a debugger DAP server.

This post walks through what's in the box, with code that compiles today.

Ora is a smart contract language and compiler for the EVM with two design pillars: comptime over runtime—decide as much as possible at compile time, so runtime is the fallback—and formal verification and the solver in the developer workflow, the way Foundry put serious testing into the Solidity workflow. FV and Z3 aren’t a separate research step; they’re in the loop: specs next to code, SMT reports in the build artifacts, counterexamples when a proof fails. Here’s what that looks like.