A research language I'm building with AI in the loop, and how I keep the AI from quietly breaking it
Work in progress, solo developer, so the usual caveats apply. I want to share the project but mostly the workflow question.
I'm building Yon, a programming language with a real type-checker (dependent types, identity/path types, a small proof kernel) that compiles to native code through MLIR and LLVM. I use AI as a pair formalizing logic and math solutions, generating code, exploring designs, drafting docs. The hard problem isn't getting the AI to write code. It's that in a system like this, AI-generated code can be plausibly wrong: it compiles, it looks right, and it silently makes the type-checker accept things it shouldn't. In a proof kernel that's the worst failure mode, because the whole point is to reject false statements.
So the workflow I've settled into is built around not trusting any single pass, AI-written or mine:
- Every claim gets verified against the code, never from memory or from what the AI "says" it did. File and line, or it didn't happen.
- An adversarial audit pass where I go hunting for false-accepts in the checker. Recent ones I found and closed: the universe-equality check was a tautology (it accepted
Type_0 == Type_5), and a naturality check reported a false "proven" from key aliasing. Neither was a crash. Both were the system claiming something untrue. No amount of "the AI wrote it and it compiled" catches these; only reading it does. - A regression suite that runs the whole pipeline end to end on every example, on Linux x86-64 and macOS Apple Silicon, plus kernel oracles. AI slop doesn't survive a regression suite. That's the filter.
The takeaway I'd offer the sub: AI is genuinely fundamental for a project this size, but only if you treat its output as a suspect that has to earn trust through mechanical verification, exactly like you'd treat your own tired 2am code. The leverage is real; the guardrails are non-negotiable.
Where it's at: this is the current line of work. Version coming in the next stretch, and I'm rewriting the site and the documentation, plus a proper illustrative project. Repo's open if anyone wants to look at how the verification side is wired.
Repository: https://github.com/yon-language/yon
Website: https://yon-lang.org/
Subreddit: r/YonLang