How a frustrating “sorry my bad” from an AI became the seed of Prove
Most programming languages weren’t built for humans. They were built with computers at the center — every decision optimized for what machines can parse, not what developers can think. We’re forced to translate our intent through a layer of syntax that was designed for compilers, not comprehension.
Then there’s AI. It generates code at an unprecedented scale, but it’s trained on our collective work without consent. The more we rely on it, the more we lose: innovation slows, open source dies, and we’re frozen at the exact moment each LLM was trained. When everyone stops writing code, nothing new gets invented.
I started Prove conceptually six years ago. These frustrations built up, but the real trigger came when I shipped code an AI had written — code with strict rules, that still failed. The AI’s response? “Sorry my bad.”
That’s when it hit me: I used AI out of laziness, but I’d bear the responsibility for its failures. The lack of accountability was the final straw. I realized we need languages that make intent explicit — where code can’t be faked, where the compiler enforces understanding.
The Verb Pattern
Look at most codebases: validate_email, new_email, get_email. We write the word “email” three times because we need unique names. The fn/def/function keywords tell us what something is — but we already knew that as humans, it’s the compiler that need the fn/function statement.
Prove uses verbs instead: validates, transforms, reads, creates. A function’s purpose is in its signature, not a prefixed name. The compiler enforces it. You can’t claim to validate something and secretly modify state.
The Explain Statement
Here’s where it gets wild. The explain statement isn’t just documentation — it’s executable natural language. The compiler parses it and translates it directly to code execution.
outputs update_email(id Option<Integer>) User:[Mutable]!
ensures valid user(user)
requires valid id(id)
explain
we get an email address
we fetch the user
then we validate the email format
we set the email to user
save and return the user
from
email as Option<Email> = email()
user as User:[Mutable] = user(id)!
set_email(user, email)
save(dump_user(user))
userThe compiler understands each phrase — get user maps to user(id)!, validate email maps to type boundary checks, set email maps to set_email(...). It’s natural language that becomes the code. The contracts (requires/ensures) verify the translation is correct.
For a complete working example with all the supporting types and functions, see the documentation.
Documentation can lie. This can’t — because the compiler checks it against the actual implementation.
But there’s something else that makes explain powerful that isn’t obvious at first: it’s editable code, not a conversation.
When you use AI to write code, every change is a fresh prompt. You ping-pong with the AI to maybe get a working result, and each refactor requires re-explaining everything from scratch. With explain, you’re writing source code. One small edit propagates consistently across your entire codebase.
Here’s the thing that gets me excited: as your codebase grows, the compiler can start suggesting functions that fit your intent. The explain statement becomes a query against your library — “I need to transform X by Y” auto-completes to functions that actually do that. Every well-documented function you write makes the next one easier. The more complete your library, the less you need to write explicitly. AI can generate correct code from intent, but only if the building blocks exist. Each explain + implementation pair builds those blocks.
Why Self-Hosting Matters
When a language compiles itself, it’s not a toy anymore — it’s a statement that the language works. Prove can express its own complexity. That’s the foundation for what comes next.
The Road Ahead
This is just the beginning. Every problem I hit while writing the compiler becomes a new feature. Refinement types, binary ASTs (un-scrapable), the verb system, contracts-as-tests — they’re all responses to real pain.
If you’ve ever felt the frustration of code that “just works” without understanding, or watched AI slop pollute your codebase, or wondered why we still write code the same way we did in the 70s — that’s why Prove exists.
It’s not about replacing developers. It’s about languages that respect them.
Prove is an intent-first programming language. If it compiles, you understood what you wrote. If it’s AI-generated, it won’t.
Leave a Reply