Ora v0.2: Sum Types, Honest Verification, and a Real Trait Surface
· 12 min read
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.