The LLM-Maximizing Principle¶
If your AI writes code without hesitation and your compiler guards the gate — why prove anything less than everything?
The Insight¶
Large Language Models generate code effortlessly. They understand patterns, follow conventions, and produce syntactically correct programs at speeds no human can match. But they also hallucinate, miss edge cases, and introduce subtle bugs that pass code review.
The traditional response: more tests, more reviews, more tooling bolted onto the side.
MVL's response: maximize what the compiler can prove.
Every property the compiler verifies is a category of bugs that cannot exist. Not "caught by tests" — structurally impossible. The LLM can try to generate a null pointer dereference, a data race, a secret leak. The code won't compile.
The Principle¶
The LLM-Maximizing Principle:
Design the language so the compiler verifies the maximum possible properties at compile time, making the LLM's job easier (well-defined constraints) and the output safer (compiler-proven guarantees).
This inverts the usual trade-off. Traditional languages optimize for human ergonomics — brevity, flexibility, expressiveness. MVL optimizes for verification density per token. The code is verbose. The LLM doesn't mind. And every annotation it generates is a property the compiler can now prove.
Well-Formed vs. Validated¶
Borrowing XML terminology:
| Property | Meaning | Who checks it | When |
|---|---|---|---|
| Well-formed | Structurally sound | Compiler | Compile time |
| Validated | Semantically correct | Tests | Run time |
In XML: well-formed means tags balance. Validated means content matches the schema.
In MVL: well-formed means the 11 requirements pass. Validated means the program does what the spec says.
Every requirement the compiler enforces is a category of tests you never write. Well-formedness reduces the validation surface. If the compiler proves no null pointers exist, you don't write null-check tests. If the compiler proves no data races, you don't write concurrency tests for race conditions.
The eleven requirements maximize well-formedness. Tests handle validation.
The Economic Shift¶
Traditional view: annotations are expensive (developers must learn and write them).
LLM view: annotations are free (the model generates them as easily as any other token).
This changes the calculus entirely:
| Era | Annotation cost | Verification value | Trade-off |
|---|---|---|---|
| Human-written code | High (learning curve, typing) | High (catches bugs) | Minimize annotations |
| LLM-generated code | Zero (just more tokens) | High (catches bugs) | Maximize annotations |
There's no reason NOT to require effect declarations, refinement predicates, ownership markers, and information flow labels when the LLM generates them for free.
The Four Pillars¶
MVL implements the LLM-maximizing principle through four integrated pillars:
-
Compile-Time Verification
The 11 requirements: type safety, memory safety, null elimination, effect tracking, ownership, termination, data race freedom, refinement types, information flow control, exhaustive matching, error visibility.
-
Testing Suite
Built-in unit tests, property-based testing, BDD scenarios, MC/DC coverage analysis, and fuzzing. Not bolted on — language-level features.
-
Build-Time Assurance
SBOM generation, license validation, extern-rationale requirements, supply chain audit. Every build produces auditable artifacts.
-
Runtime Observability
Structured logging with package context, audit trails for IFC label crossings, metrics, distributed tracing. Observability by default, not by effort.
The Result¶
Code that compiles is well-formed across all eleven properties. Tests verify it does the right thing. Builds produce supply chain evidence. Runtime emits structured telemetry.
The LLM handles the syntax. The compiler handles the proof. The toolchain handles the evidence.
This is what "designed for AI generation" means in practice.