Lyric Writes Lyric
The moment a language starts building its own tools.
This is the second post about building Lyric, a new programming language, with Claude Code. The first covered the initial three days: a working compiler, 690 tests, and the observation that the time to a credible bootstrap had collapsed by roughly two orders of magnitude compared to the histories of Go, Kotlin, Rust, and Swift.
That post ended with a list of things still deferred: real async state machines, a proper package manager, a formatter, reflection-driven FFI (Foreign Function Interface). Those were accurate deferrals at the time of writing.
All four have shipped since. I’m writing this on the 5th of May.
But that’s not what this post is about.
The moment that changed the frame
Somewhere in the second half of this week, Lyric crossed a line that most languages don’t cross for years, and some never cross at all. It started writing its own tools.
compiler/lyric/jvm/ is a directory of Lyric source files. They implement a JVM (Java Virtual Machine) bytecode emitter: the thing that would allow Lyric programs to run on the Java Virtual Machine, not just the .NET runtime the compiler currently targets. There is no F# doing the heavy lifting. The F# side of the compiler has a five-line path-resolution shim that locates the source files. Everything else, including the class-file data model, the binary serializer, the full opcode table, and the bytecode assembler, is 1,619 lines of Lyric spread across four packages.
Jvm.Kernel is 162 lines of byte-list primitives: the foundation. Jvm.Classfile is 385 lines implementing the §4 class-file data model and binary serializer, with records for ClassFile, FieldInfo, MethodInfo, attributes, and the serializeClass function that produces a List[Byte] a real JVM will accept as a valid .class file. Jvm.Bytecode is 999 lines covering every JVM opcode, the AsmInsn union type, the MethodAssembler builder, and typed emitter functions for every major instruction category: loads and stores, arithmetic, field access, all five invoke forms, branches, object creation, and returns.
The class-file serializer is complete and working. The bytecode assembler compiles and is structurally correct. Hello World is written. The test constructs the bytecode, writes Hello.class to disk, and hands it to javap -c to verify the bytes are structurally valid.
It isn’t running yet. The two-pass assembler (buildLabelMap then emitAllInsns) does a match over the AsmInsn union in statement position, and the .NET (Microsoft’s cross-platform successor to the .NET Framework) emitter has a codegen bug with that pattern. The Lyric code is correct. What’s broken is the compiler’s own lowering of that specific case.
A language that is almost self-hosting exposed a bug in its own compiler. That’s the state of things, and it’s a more interesting state than “working” would have been.
Why self-hosting matters
The conventional milestones for a language’s maturity run roughly as follows. First, a bootstrap compiler (typically written in a different language) that can compile a meaningful subset of the new language. Then a growing standard library, tooling, and documentation. Then, eventually, self-hosting: the compiler is rewritten in the language it compiles, which is the moment the language becomes its own primary development environment.
Go achieved self-hosting in 2015, eight years after the project started. Rust’s compiler was fully written in Rust by around 2011 to 2012, roughly five years in. These are considered significant milestones because they demonstrate that the language is expressive and stable enough to handle real systems programming workloads, not just worked examples.
Lyric’s JVM emitter is not a self-hosted compiler. To be precise: it is a 1,619-line systems program written entirely in Lyric, implementing a non-trivial binary format, doing two-pass assembly, and nearly producing valid JVM bytecode. It is the first sign of the capability, not its completion. But it appeared at day five, not year five. And it appeared because Lyric the language was expressive enough to write it: the generics, the sum types, the pattern matching, the FFI layer, all of which have been working for days.
The codegen bug blocking Hello World will get fixed. When it does, the JVM emitter will run, and Lyric will produce valid Java bytecode from Lyric source. The plan document for that work (docs/18-jvm-emission.md) runs to §23 and covers the full lowering of generics, async, distinct types, and the rest. That is a long road. But the road started at day five.
The book
A language with a working compiler is a technical achievement. A language with a book is something a developer can actually learn.
The Lyric Language book is 19 chapters, two appendices, and approximately 5,600 lines of markdown. It is organised in seven named parts, explicitly progressive; the preface says so directly, and means it. Part I covers the toolchain and first programs. Part II covers the core language: types, data structures, functions, pattern matching, modules. Part III begins the safety argument: error handling, contracts, opaque types. Part IV covers the things you need for real programs: async, concurrency, dependency injection, the standard library, FFI. Part V covers testing and quality. Part VI is verification. Part VII is the package ecosystem.
The book’s target reader is named in the preface without ceremony:
“You know how to program. You are comfortable with at least one statically-typed language: Java, C#, Kotlin, TypeScript, Scala, Rust, Go, something in that neighbourhood. You have written code that runs in production. You are not here to learn what a function is.”
Every chapter has an exercises section. All 19, no exceptions. The exercises are not illustrative; they are actionable. The Chapter 17 exercises on proofs have you run lyric prove --json, read the counterexample output, add a postcondition, run again, and trace the progression. The Chapter 8 exercises on contracts have you deliberately break postconditions and observe the specific runtime violation message for the first requires: clause versus the second. These are “open your editor and type this, then observe what happens” exercises with specific observable outcomes.
The proof system is not an advanced optional chapter. It gets two full chapters (17 and 18) and is the culmination of the book’s argument, listed in the preface as one of the four things a working developer probably hasn’t done before, alongside nominally distinct types, structural contracts, and compile-time dependency injection. Chapter 17 opens: “@runtime_checked catches violations for the specific inputs the program runs with. @proof_required catches them for every possible input, before the program ever runs.”
A banking example threads through the book from Part III onwards. It first appears in Chapter 7 (error handling), reappears in Chapter 8 (contracts), and culminates in Chapters 17 and 18 where the conservation invariant (that money is neither created nor destroyed by a transfer) is proven correct for all possible inputs using the SMT (Satisfiability Modulo Theories) backend. A reader who works through the book from the beginning arrives at a formal proof of a real domain invariant having built up to it over twelve chapters. That’s not a toy exercise.
The proof system in numbers
The first post mentioned the proof system as a deferred Phase 4 item. It shipped in 48 hours once I directed Claude Code to stop deferring it.
The pipeline runs weakest-precondition calculus over Lyric’s imperative fragment, emits SMT-LIB (Satisfiability Modulo Theories Library) v2.6, and discharges goals on two paths: a trivial syntactic discharger for tautologies, reflexivity, and hypothesis matches (no external dependency required), and a Z3 shell-out for arithmetic obligations. When Z3 produces a counterexample, it’s parsed and shown inline. V0008 Counterexample is always a hard error. V0007 Unknown (arithmetic goal, Z3 unavailable) degrades to a warning with --allow-unverified, keeping CI (Continuous Integration) green on machines without Z3 installed.
The thing I find most useful about the counterexample output is what it does to the development loop. This contract is wrong:
pub func broken(x: Int): Int
requires: x >= 0
ensures: result < x
= x * xZ3 produces: x = 0, result = 0, expected result < 0. Zero squared is zero, which is not less than zero. The contract said the result would always be smaller than the input, and the tool found the specific witness that disproves it. That feedback loop, write a contract, run lyric prove, get a counterexample with a concrete value, is the thing that makes the proof system feel like a development tool rather than an academic exercise.
The Verifier suite alone has 242 tests. The repository total is now 1,392 across seven suites, up from 690 at the first post. The progress log is at entry D-progress-092, up from D-progress-032: sixty new entries in two days.
What I directed, and what that means
The first post described a collaboration where I directed on a handful of design decisions and let Claude Code make implementation choices autonomously. That was accurate for the first three days.
The shift in the second half was not that I started writing more code; I didn’t. It was that I stopped accepting “bootstrap-grade scope” as an answer for things that were actually buildable. The proof system was the clearest case: Phase 4, months 39 to 57 per the original plan, not blocking v1.0. My instruction was simple: build it anyway. It shipped in 48 hours.
The same pattern applied to the async state machine, the package manager, the formatter, and the reflection-driven FFI. Each of these had been deferred to a named phase. Each shipped once I pushed past the deferral.
The one case where I overrode a specific implementation choice rather than a scope decision: the VCGen (Verification Condition Generator) had a bug where early return branches in an if-expression were substituted with true (Bool) rather than the actual return value. The proposed fix was to rewrite the example function to avoid early return. My override was to fix the VCGen instead. The fix was six lines; there is now a regression test. A workaround would have introduced silent unsoundness for any Lyric programmer writing natural early-return style in a @proof_required function. That distinction between a local patch and a correct fix is the kind of call that has to come from the human side of the collaboration.
What remains genuinely deferred: CLR (Common Language Runtime) generic constraints are still enforced at monomorphisation call sites rather than lowered to CLR constraint metadata (a Phase 5 target). Async lambdas and closures are not yet synthesised by the state machine emitter. The proof story is sequential per function entry, so concurrency verification (specifically protected type schedule fairness) is out of scope for Phase 4. LSP (Language Server Protocol) counterexample UX, the --explain JSON schema and inline fix-its, is post-v2.0 polish. These are specific gaps in specific features, not entire phases of the plan sitting untouched.
Where things actually are
Five days in. One working compiler. A JVM emitter written in Lyric, blocked on one codegen bug it exposed in its own compiler. A 19-chapter book with exercises in every chapter. A proof system that discharges contracts and produces counterexamples. A package manager. A formatter. A Language Server Protocol implementation. 1,392 passing tests.
The original implementation plan had all of this across five phases spanning roughly seven years, with a proof system requiring a funded specialist team and formal methods expertise. The plan was written before a single line of compiler code existed, when the comparison points were Go and Rust and Kotlin: languages built by large teams over half a decade.
The plan was wrong about what the constraint was. It wasn’t time or expertise. It was ambition and direction.
Lyric the language is now expressive enough to write significant programs in itself. One of those programs is implementing a compiler backend. The bug it found was in the compiler it depends on. That feedback loop, where a language finds a gap in its own toolchain, is what self-hosting actually means in practice. It usually takes years to get there.
It took five days to get close enough to matter.
The repository is at github.com/nichobbs/lyric-lang. The JVM emitter source is compiler/lyric/jvm/. The book is docs/book/. The verifier is compiler/src/Lyric.Verifier/.