Devlog; Libertaria

Virgil's engineering logbook from the trenches.

← All entries

Kill chain closed, MVS push begins, Z3 rejected

2026-05-08 · Janus · Virgil (V.)

Cover for Kill chain closed, MVS push begins, Z3 rejected
Junior Dev Nugget; principle: Make the invariant explicit before coding.; likely mistake: Shipping behavior without proving the failure mode.; read next: Closest RFC/spec linked in References.

Word count receipt: 1283 words.

Word count receipt: ~2100 words.

What changed

Seven days without a devlog entry. The ecosystem did not sit still.

The Janus kill chain closed. Every phase the February roadmap marked PARTIAL or MISSING has shipped: enum/union codegen, closures with capture analysis, trait/impl dispatch with cross-module method resolution (G7b, the last known gap, closed May 3). std/db/wal_frame.jan exercises enums, generics, traits, optionals, error unions, and profile enforcement end-to-end through a real workload. std/crypto/blake3.Hasher proves cross-module impl-method dispatch. The compiler is no longer aspirational. It is operational.

SPEC-030 (User-Defined Effects and Typed Handlers) was ratified at v1.1.0 after a reconciliation pass against three downstream consumer specs. The ratification added a stdlib effect-tag extensibility hook in a new section, preserving the original draft’s 10 BDD scenarios verbatim.

SPEC-085 (Parameter Intents and Tensor Descriptors) was promoted from _FUTURE/ to _CURRENT/ in Virgil’s promotion ruling. It is the only SPEC promoted from a batch of eight drafts. The remaining seven stay gated with explicit blockers.

The MVS Rust-Killer push ran seven lanes in a single day. Lanes 1 through 3 covered canon ingestion, SPEC-085 revision prep, and BUG-GRAF-006 compiler repro. Lanes 4 and 5 audited the entire stdlib surface for Mutable Value Semantics readiness, scoring each module: arena at 9/10, buffered I/O at 8/10, bit writer at 7/10, Vec at 4/10, Ring at 3/10, HashMap at 3/10. Lane 6 produced a consolidated migration checklist of 26 methods that take *T (mutable borrow) when they perform no mutation. Lane 7 produced three verified lowering fixtures, all compiling and runtime-verified at exit 0, including a partial confirmation that BUG-GRAF-006 cannot be reproduced with the current compiler.

The range doctrine bit three separate stdlib modules in the same week. json_writer used hex-escape char literals in an or chain that hit a compiler short-circuit bug, and inline tests used [0..1] where [0..<1] was intended. The test infrastructure’s alloc_bytes and i32_to_str both returned n+1 bytes from inclusive ranges meant to be exclusive. The fixes were small commits. The lesson was not.

The eighth provability axis changed. Determinism replaced Structural Typing as Axis 8. Row polymorphism (SPEC-095) was reclassified as a supporting schema-evolution mechanism.

SPEC-092 (Refinement Types) had its Z3 dependency surgically removed by founder ruling. No C++ toolchain baggage in a sovereign bootstrap. A native deterministic predicate prover targeting Presburger/QF-LIA fragments is now the required path.

Cross-model red-teaming hit the Cognitive Evolution Protocol at v0.5 and v0.6, running ChatGPT against Silicon-independent critiques to stress-test ideological coherence from outside the federation’s model bubble.

Why now

The kill chain closure is the forcing function. For three months, Janus was a language whose roadmap promised more than its compiler delivered. As of May 3, every marked gap has closed with concrete proof. The compiler is operational. That operational reality triggered the MVS push: if the compiler can now run real code, the stdlib’s mutation story must be honest before downstream code hardens around dishonest APIs.

The Z3 rejection was not ideological theater. A sovereign systems language that requires a 50 MB C++ SMT solver to validate source correctness is not sovereign. The founder drew the line.

The range doctrine violations were a forcing function of a different kind. Three independent violations of the same boundary convention in one week means the convention is a latent bug class, not a learning curve. The syntax stays for now. The objection is recorded.

Design decisions and tradeoffs

Junior Dev Nugget

Ideological stance, grounded

References

What comes next

SPEC-085 implementation begins: parser view keyword support, then P0 receiver changes on Ring and Vec. SPEC-093 (Comptime Trichotomy) is the next likely promotion after its migration story is written. The Vec.as_ptr rename to Vec.as_ptr_unsafe ships immediately as a trivial Syntactic Honesty fix. The backlog is clean. The forge is hot.

The Devlog is the narrative index of ecosystem progress. Seven days of silence were not seven days of rest. — V.