What Should Humans Design When AI Can Write Most of the Code?
AI can now write code.
Not perfectly. Not always safely. Not without review.
But it can write a great deal of code.
It can generate functions, create tests, call APIs, build UI components, handle common errors, and produce large amounts of implementation detail at a speed no human developer can match.
This changes the meaning of programming.
For a long time, much of a programmer's work was the act of implementation itself. We read requirements, understood the system, designed functions, wrote types, created tests, handled edge cases, debugged errors, and gradually transformed an abstract idea into working code.
Of course, programming was never only typing. It always required design, judgment, and understanding.
But still, a large amount of time was spent translating structure into code.
Now AI is starting to take over a large part of that translation work.
So the question is not simply:
Can AI write code?
The more important question is:
If AI can write most of the code, what should humans design?
My answer is this:
Humans must design the structure that comes before code.
AI can generate implementation.
But humans still need to define what the correct structure is.
What states exist in the system?
What operations are allowed?
What invariants must always hold?
What must be true before an operation is executed?
What must be guaranteed after it completes?
When multiple AI agents work together, what contract connects their outputs?
These are not merely coding questions.
They are specification questions.
And this is where my current research and development work begins.
The Limitations of Natural Language Specifications
When people use AI to build software, they often describe what they want in natural language.
For example:
Build an order management system.
Do not allow an order if inventory is insufficient.
Confirm the order when payment succeeds.
Do not allow a canceled order to be confirmed again.
At first glance, these instructions seem clear.
But as software specifications, they are full of ambiguity.
What exactly does "insufficient inventory" mean?
At what moment is inventory checked?
Is inventory reserved before payment or deducted after payment?
What happens if payment fails?
Can a canceled order still be refunded?
What state transitions are valid?
What assumptions does the payment module make about the order module?
What assumptions does the inventory module make about the payment module?
Human developers may notice these ambiguities during conversation.
But when AI agents are asked to implement different parts of the system independently, ambiguity becomes dangerous.
Imagine one AI agent implementing the order module.
Another implements inventory.
Another implements payment.
Another writes the UI.
Another generates tests.
Each agent may interpret the same natural language instruction slightly differently.
Individually, each piece of code may look reasonable.
But when the modules are integrated, the system may fail.
The problem is not that AI cannot write code.
The problem is that the structure given to AI is often ambiguous.
Natural language is flexible.
That is why humans like it.
But software systems require precise boundaries.
And AI agents need contracts they cannot easily misinterpret.
Formal Specifications as the Skeleton of Software
This is why I am interested in applying formal methods to AI-assisted software development.
Formal methods allow us to describe software specifications with mathematical precision.
Among them, I am particularly interested in VDM-SL.
VDM-SL allows us to define:
- types
- state
- invariants
- operations
- preconditions
- postconditions
In other words, it allows us to describe what a system is supposed to be before we write the implementation.
To me, VDM-SL is not merely an old formal specification language.
It is a language for giving structure to AI.
Natural language is too ambiguous.
Implementation code is too concrete.
Formal specification sits between them.
It is not yet executable application code.
But it is much more precise than ordinary prose.
A formal specification describes the skeleton of a system.
Before asking AI to write code, we define the skeleton.
After AI writes code, we check whether the code conforms to that skeleton.
When multiple AI agents collaborate, we use the skeleton as a contract between them.
This changes the role of the human developer.
The human is no longer just the person who writes every line of code.
The human becomes the person who defines the structure that AI must respect.
Formal Agent Contracts
One of the ideas I am working on is what I call Formal Agent Contracts.
The idea is simple:
When multiple AI agents collaborate on software development, the boundaries between agents should be defined as formal contracts.
These contracts can specify what each agent is responsible for, what data it receives, what data it returns, and what conditions must hold before and after its work.
For example, in an e-commerce system, we might have separate agents for:
- Order
- Inventory
- Payment
- Notification
- UI
- Testing
Without formal contracts, each agent may generate code based on its own interpretation of the requirements.
With formal contracts, each agent works against a clearly defined boundary.
The order agent knows exactly what an Order state is.
The inventory agent knows exactly when stock can be reserved.
The payment agent knows exactly what must be true before payment confirmation.
The test agent knows what properties the system is supposed to satisfy.
The point is not to restrict AI unnecessarily.
The point is to give AI enough structure to work safely.
Freedom without contracts creates chaos.
Freedom within contracts creates collaboration.
From Test-Driven Development to Formal-Spec-Driven Development
I do not think tests are obsolete.
Tests are still essential.
They are useful for checking examples, integration behavior, UI behavior, external API interactions, performance, and real-world use cases.
But in AI-assisted development, tests alone are not enough.
Tests check finite cases.
Formal specifications describe properties.
A test says:
For this input, the output was correct.
A formal specification says:
This operation must always preserve this invariant.
When AI can generate large amounts of code very quickly, we cannot rely only on testing generated code after the fact.
We need to define the structure before code is generated.
This is why I am interested in formal-spec-driven development.
The workflow looks like this:
- A human describes the domain rules.
- AI helps translate those rules into a formal specification.
- The human reviews whether the specification matches the real domain.
- Formal tools check the specification for consistency.
- AI agents generate implementation based on the specification.
- Tests and reviews verify that the implementation follows the intended behavior.
In this workflow, AI is not replacing human judgment.
AI is assisting with translation, implementation, and verification.
The human remains responsible for meaning.
Why AI Makes Formal Methods More Practical
Formal methods have existed for a long time.
They have been used in safety-critical and high-reliability systems.
They are powerful.
They can reveal errors that ordinary testing may miss.
But they have not become mainstream in everyday software development.
Why?
Because they are difficult.
Writing formal specifications requires training.
Many developers are not familiar with mathematical notation.
The tooling can feel unfamiliar.
The short-term cost often seems too high compared with simply writing code and tests.
AI may change this.
AI can help write formal specifications.
AI can explain formal specifications in natural language.
AI can help translate domain rules into VDM-SL.
AI can interpret verification errors.
AI can generate implementation scaffolds from specifications.
This means AI may reduce the adoption barrier of formal methods.
At the same time, formal methods can reduce one of the biggest risks of AI-generated code: ambiguity.
AI makes formal methods easier to use.
Formal methods make AI-generated software safer to trust.
That mutual relationship is what interests me.
Humans Move Upstream
In AI-assisted development, humans do not disappear.
They move upstream.
From writing every line of code
to defining the structure of the system.
From implementing details
to deciding state, constraints, and contracts.
From checking only examples
to defining properties that must always hold.
From giving vague prompts
to designing specifications that AI cannot easily misunderstand.
This does not make human developers less important.
It makes their judgment more important.
AI can generate code.
But it cannot reliably decide what the business rules should be.
AI can produce implementation options.
But it cannot fully understand the long-term maintenance cost of a wrong abstraction.
AI can write tests.
But it cannot always know whether the test represents the real-world domain correctly.
AI can assist with formal specifications.
But the human must still decide whether the specification captures the intended meaning.
The human role becomes more architectural, more semantic, and more responsible.
Specification as a Shared Object Between Humans and AI
One of the biggest problems in AI-assisted development is that natural language prompts are not stable enough as shared objects.
A prompt is easy to write.
But it is also easy to misread.
Different humans may interpret the same prompt differently.
Different AI agents may produce different assumptions from the same prompt.
And once the code is generated, the original intention may disappear into implementation details.
A formal specification can act as a shared object.
It is readable by humans, at least with support.
It is processable by tools.
It can guide AI generation.
It can be checked, revised, and versioned.
It can define the contract between modules and agents.
This is important because AI development is becoming less like a single programmer writing a single file.
It is becoming more like orchestration.
Multiple agents.
Multiple modules.
Multiple generated artifacts.
Multiple layers of verification.
In such an environment, we need something more stable than a prompt.
We need contracts.
My Research Direction
My work is not simply about promoting VDM-SL.
It is not only about building a Claude Code plugin.
It is not only about making AI coding more convenient.
The deeper question is:
How should software development be reorganized when AI can generate implementation?
My answer is:
We need a formal layer between human intention and AI-generated code.
That layer should express:
- domain rules
- states
- invariants
- valid operations
- module boundaries
- agent responsibilities
- preconditions
- postconditions
- properties that must be preserved
This formal layer allows humans, AI agents, and verification tools to cooperate.
Humans provide meaning.
AI helps translate and implement.
Formal tools check consistency.
AI agents generate code.
Humans review the result against the intended structure.
This is not development without humans.
It is development where humans work at a higher level.
Why This Matters
As AI-generated code becomes more common, the amount of software being produced will increase dramatically.
But more code does not necessarily mean better systems.
If the structure is wrong, AI will generate wrong code faster.
If the requirements are ambiguous, AI will multiply ambiguity.
If module boundaries are unclear, AI agents will produce incompatible pieces.
If invariants are not defined, errors may only appear late in integration or production.
Speed without structure is dangerous.
That is why I believe formal specifications will become more important, not less.
The future of software development is not simply:
AI writes code.
It is more likely:
Humans define structure.
AI generates implementation.
Formal specifications connect intention, verification, and code.
Conclusion
AI can now write much of the code.
So human developers must ask a new question:
What remains uniquely important for us to design?
I believe the answer is structure.
The structure of states.
The structure of constraints.
The structure of operations.
The structure of responsibility between modules.
The structure of contracts between AI agents.
Code is no longer the only central artifact.
The specification before code may become just as important.
Perhaps even more important.
My work explores this transition:
From implementation-first development
to formal-spec-driven development.
From vague natural language prompts
to verifiable contracts.
From AI as a code generator
to AI as a collaborator constrained by formal structure.
From humans as manual coders
to humans as designers of meaning, correctness, and architecture.
AI can write code.
But humans must still decide what the code is supposed to mean.