The Linguistic State Explosion
Eliminating logic bugs requires the software industry to adopt strict linguistic constraints instead of scolding engineers for misinterpreting English.
By Leo Marchetti
Sparked by Agent Skill to Force Docs in ASD-STE100 Simplified Technical English · discussion
The other day an aviation mechanic introduced me to ASD-STE100, the aerospace standard for writing technical manuals. I spent the weekend reading about the 1980s origins of AECMA Simplified English and the culture shock it induces. Back then, European airlines were buying planes from American manufacturers, and maintenance crews across the continent were struggling to parse wildly idiomatic, complex manuals.
When software engineers see this standard discussed online today, they bristle. In a recent Hacker News discussion thread, community reactions immediately compared the constraints to George Orwell's Newspeak, dismissing the rules as draconian stylistic pedantry and over-engineering.
Aerospace engineers adopted these strict linguistic constraints for a much simpler, bloodier reason: mechanics were accidentally blowing up engines. Ambiguous English was physically killing people. When a manual says "replace the valve if it is leaking or damaged and test the pressure," a non-native speaker—or just a tired mechanic on a night shift—has to guess the order of operations and the binding of those adjectives.
Software engineering routinely ignores the mathematical reality of human language. To see why, let's map an everyday software requirement directly into a formal model. Imagine a standard Jira ticket sitting in a sprint backlog: If the transaction times out, the system should retry or abort and alert the user.
(I know, your product manager writes flawless acceptance criteria and you always refine edge cases perfectly in sprint planning. Just humor me; we are isolating the math of ambiguous phrasing, not auditing your agile rituals.)
Let's write a naive TLA+ model using the PlusCal algorithm language. We will literally map the English sentence directly to state transitions. We just want to formally ensure that if a transaction aborts, the user receives an alert, and if it retries successfully, they remain blissfully unaware.
---- MODULE NaiveSpec ----
EXTENDS TLC
VARIABLES status, alert_sent
(*--algorithm JiraTicket
begin
Timeout:
\* "retry or abort"
either
status := "retry";
or
status := "abort";
end either;
\* "and alert the user"
alert_sent := TRUE;
end algorithm; *)
Correctness == (status = "retry" => alert_sent = FALSE)
====
How does the model checker interpret this? The either...or block in PlusCal allows TLC to explore every possible non-deterministic branch. If the ticket says "retry or abort", the checker is going to simulate a universe where we retry, and a parallel universe where we abort. Then it hits the second half of the sentence: "and alert the user."
If we compile and run TLC to check our literal translation of the English syntax against our correctness invariant, we can watch it process the logic exactly as written.
Error: Invariant Correctness is violated.
The behavior up to this point is:
State 1: <Initial predicate>
status = "timeout"
alert_sent = FALSE
State 2: <Timeout line 9>
status = "retry"
alert_sent = TRUE
We just spammed the user for a background system recovery.
What happened? The natural language ambiguity creates a <dfn>Linguistic State Explosion</dfn>. The phrase "retry or abort and alert" allows multiple valid abstract syntax trees to form in the reader's head. Does the alert binding attach strictly to the abort clause? Or does the conjunction bind to the entirety of the preceding conditional? The model checker explores the literal syntax and predictably finds a legal path where we alert a user about a successful retry as if it had failed entirely.
The English language just allowed a bugnuts crazy combinatorial state machine to slip right past our mental parser. We intuitively apply implicit parentheses where none mathematically exist, assuming the requirement reads as (retry) OR (abort AND alert). But the system reads it left-to-right, executing (retry OR abort) AND alert.
Think about how hair-pullingly frustrating this is in a real codebase. The developer reads the ticket, builds the left-to-right interpretation, and ships it. The QA engineer reads the exact same ticket, applies the implicit grouping, and fails the build. Two entirely rational actors compiled the same English sentence into two mutually exclusive execution paths.
This brings us right back to the aviation mechanics. The aerospace fix from the ASD-STE100 guidelines is beautifully uncompromising: Put a condition before an instruction.
In the physical world, this grammatical rule literally stops a mechanic from pulling a lever before reading the conditional safety check. In the formal verification world, it completely collapses our branching logic. By forcing the condition before the action, we eliminate the dangling modifier problem that plagues our error handling. Let's rewrite the English requirement by strictly applying the aerospace STE rules.
If the transaction times out, retry the transaction. If the retry fails, abort the transaction. If the transaction aborts, alert the user.
Notice how stiff and robotic that feels? That is the sound of ambiguity dying. Now let's model this properly constrained version, mapping the new linear syntax directly into PlusCal.
---- MODULE ConstrainedSpec ----
EXTENDS TLC
VARIABLES status, alert_sent
(*--algorithm JiraTicketSTE
begin
Timeout:
status := "retry";
RetryCheck:
if status = "failed" then
status := "abort";
end if;
AlertCheck:
if status = "abort" then
alert_sent := TRUE;
end if;
end algorithm; *)
Correctness == (status = "retry" => alert_sent = FALSE)
====
Model checking completed. No error has been found.
2 states generated, 2 distinct states found.
It passes perfectly. By adopting an aerospace constraint, we force a nonmonotonic set of assumptions into a deterministic, linear sequence. We mathematically collapse a sprawling, explosive probability tree into a single, unambiguous path.
When an engineer implements the wrong logic from a Jira ticket, management almost always treats it as a moral failing. The developer didn't read carefully enough. They rushed the ticket. They lacked attention to detail.
But forcing a human brain to parse implicit algebraic precedence out of conversational English isn't a character test. It is a tooling and UX problem. We are using an inherently lossy, ambiguous user interface—natural language—to construct rigid state machines. We demand developers translate this squishy interface into flawless logic using nothing but their own mental RAM, and then get mad when they drop a pointer.
The aviation industry didn't solve engine fires by telling mechanics to try harder; they patched the English language. If we actually care about software correctness, we have to stop scolding engineers for being bad at mental combinatorics. We need to start treating specification as the UX problem it actually is, and give developers the grammatical constraints they need to survive.