2 posts tagged with "adt"

Ora v0.2 is the release where the pieces start to act like one system.

The headline features are big on their own: first-class Result<T, E> values, a unified ADT model, Z3-backed verification reports, runtime ABI encoding, dynamic public returns, traits, debugger improvements, LSP production work, compiler metrics, CFG output, and a real MLIR optimization pipeline.

But the real v0.2 story is simpler: Ora is moving from "a compiler with verification features" toward contracts that carry their proof obligations, their runtime checks, their ABI shape, and their debugging evidence through one pipeline.

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.