When I saw the title, I thought this was maybe going to be an overview of things like Z and MALPAS, and program-proving tools!
My high school had an elective in predicate calculus (and a later elective in Algol-60 programming), and I got very into Prolog for logic programming at university. My first job, post-graduation, exposed me to MALPAS (I helped write a 3-pass C-to-MALPAS translator), and somewhere along the way I was introduced to Z but I could never really get into that.
I think I would baulk at describing most programming languages as "formal systems" tho' -- there's far too much implementation-defined and undefined behavior in programming languages in general. Even our beloved Clojure has all sorts of undefined behavior, so you can't really defend these as having formal semantics because you can still write programs that do not have well-defined semantic behavior.
I've never used program proving tools like those. I've used Z3 but never to prove a program correct.
I understand the sentiment of not considering programming languages to be formal systems. They definitely don't feel the same. Mathematical formal systems have an elegance and rigidity that programming languages usually lack. However, this is the naive definition I mentioned I had at the beginning: "formal system" means rigorously defined.
I don't think having undefined or implementation-defined behavior will bump them out of the category. They have all the things the definition says you need. The difference is that they don't feel like the good ones because they're complicated and have lots of undefined behavior. They're so complicated that they become hard to use for proofs.
BTW, I think it's interesting that there's a small cottage industry of defining the semantics of popular languages in a rigorous way, often using denotational semantics. There's some kind of core that is well-defined. Some of them simplify, but some try to contain all semantics. Featherweight Java is an example: https://dl.acm.org/doi/10.1145/503502.503505
I also think that there's a core in Clojure that is well-defined enough to use for getting that "tight ship" feeling you get from using formal systems.
Brilliant exploration of how the meaningelss variables paradox actually makes formal systems powerful! The iota combinator example really drives home why we need that balance between minimalism and readabilty. What's clever is showing how domain modeling is basically the art of choosing which parts stay meaningless to the system but meaningful to us.
Thanks for the article, very well explained. GED is an amazing book. I read it cover to cover in HS after attending a summer math program for HS students at the University of Chicago. My math TA's turned me onto it and it is what propelled me into the field of AI and the world of Lisp. The dialogues between the Tortoise and Achilles are simply hysterical. I hope you find time to read the whole book.
The part I read also got me thinking about self-reference. I don't think I appreciated the formal systems part yet. I wasn't ready back in HS when I read it.
When I saw the title, I thought this was maybe going to be an overview of things like Z and MALPAS, and program-proving tools!
My high school had an elective in predicate calculus (and a later elective in Algol-60 programming), and I got very into Prolog for logic programming at university. My first job, post-graduation, exposed me to MALPAS (I helped write a 3-pass C-to-MALPAS translator), and somewhere along the way I was introduced to Z but I could never really get into that.
I think I would baulk at describing most programming languages as "formal systems" tho' -- there's far too much implementation-defined and undefined behavior in programming languages in general. Even our beloved Clojure has all sorts of undefined behavior, so you can't really defend these as having formal semantics because you can still write programs that do not have well-defined semantic behavior.
I've never used program proving tools like those. I've used Z3 but never to prove a program correct.
I understand the sentiment of not considering programming languages to be formal systems. They definitely don't feel the same. Mathematical formal systems have an elegance and rigidity that programming languages usually lack. However, this is the naive definition I mentioned I had at the beginning: "formal system" means rigorously defined.
I don't think having undefined or implementation-defined behavior will bump them out of the category. They have all the things the definition says you need. The difference is that they don't feel like the good ones because they're complicated and have lots of undefined behavior. They're so complicated that they become hard to use for proofs.
BTW, I think it's interesting that there's a small cottage industry of defining the semantics of popular languages in a rigorous way, often using denotational semantics. There's some kind of core that is well-defined. Some of them simplify, but some try to contain all semantics. Featherweight Java is an example: https://dl.acm.org/doi/10.1145/503502.503505
I also think that there's a core in Clojure that is well-defined enough to use for getting that "tight ship" feeling you get from using formal systems.
Brilliant exploration of how the meaningelss variables paradox actually makes formal systems powerful! The iota combinator example really drives home why we need that balance between minimalism and readabilty. What's clever is showing how domain modeling is basically the art of choosing which parts stay meaningless to the system but meaningful to us.
Thanks for the article, very well explained. GED is an amazing book. I read it cover to cover in HS after attending a summer math program for HS students at the University of Chicago. My math TA's turned me onto it and it is what propelled me into the field of AI and the world of Lisp. The dialogues between the Tortoise and Achilles are simply hysterical. I hope you find time to read the whole book.
The part I read also got me thinking about self-reference. I don't think I appreciated the formal systems part yet. I wasn't ready back in HS when I read it.
Eric, this is a beautiful explanation of formal systems. What resonates most is your distinction between:
Meaningless symbols (atoms, variables, placeholders)
Meaningful structure (rules of inference, syntax trees, transformations)
Human-supplied semantics that give it all purpose
I want to connect this to the Eventz equation I work with:
y = F(Y, e).
Eventz emerged not from computer science theory but from business operations—yet it behaves exactly like a formal system in your sense.
1. Eventz has the four components of a formal system
Symbols
Data tuples—immutable, timestamped facts.
Like atoms: they contain names that mean nothing to the system itself.
Statements
The tuple archive Y, plus incoming event e.
This is the syntactic “universe” the Function sees.
Mechanistic Rules
The Function F, which must be:
pure
deterministic
total
side-effect-free
It is literally a rewrite rule:
(Y, e) → y
Axioms
The organization’s business rules.
These are the domain truths that make F meaningful.
So Eventz is not a methodology; it’s a state-transition calculus, a formal system for business behaviour.
2. Eventz embraces your point about “meaningless variables”
In Eventz, a Function F never cares about who Jim is or what Pizza is.
It cares only that:
Jim is an entity
Pizza is a food
Likes(Jim, Pizza) is a defined relationship
The meaning belongs entirely to the stakeholders, not the software.
This is exactly your distinction: structure is formal, names are human.
Business people define the domain vocabulary.
The programmer does not.
3. Eventz is a stratified system with metalinguistic abstraction “baked in”
You emphasize that formal systems support layered design:
Lambda calculus →
Lisp →
DSLs →
Domain models
Eventz does the same:
The tuple is the lowest semantic layer (neutral structure)
Functions define inference rules
Departments define the meaning of events
Organizations build higher-level behaviours by composing Functions
Every Function is a domain-specific inference rule.
Every department becomes a DSL.
4. Eventz solves a fundamental modeling problem that confounds traditional systems
You note that the real challenge is not derivation—it’s encoding meaning.
Eventz deals with this directly:
The archive Y contains every fact the organization has ever known.
The function F operates only on Y and the event e.
This eliminates hidden state, mutable objects, peer-to-peer coupling, and the accidental complexity that makes modeling so difficult.
Encoding meaning becomes:
Interview the stakeholders
Write down the events and rules
Implement each rule as a pure Function F
That’s it.
No database schemas, no microservices choreography, no transaction logic, no state machines.
Just statements + rules → new statements.
Exactly like a formal system.
5. Why this matters
You made a crucial observation:
The power of a formal system comes from what it leaves out.
Eventz succeeds for this reason:
It leaves out mutable state
It leaves out hidden side effects
It leaves out coupling
It leaves out technical frameworks and platform complexity
What remains is:
Immutable symbols (tuples)
Deterministic inference rules (Functions)
A universal dataspace (Y)
Domain-derived axioms (business rules)
In other words:
Eventz is minimal enough to be robust, and expressive enough to model any business domain.
The algebra is tiny.
The human meaning is rich.
6. Your closing point is exactly the Eventz ethos
You write:
“Domain modeling points you to a reliable source of answers: the domain itself.”
Eventz formalizes that insight.
Stakeholders describe:
The events that matter
The rules that govern them
The software becomes a formal execution of the domain, not an interpretation of a technical design.
Summary
Your article articulates the theoretical foundation for something I’ve been practicing empirically for years:
Eventz is a formal system.
Its syntax is the tuple.
Its inference rule is F.
Its semantics live entirely in the domain.
Where traditional systems accumulate accidental complexity, Eventz deliberately removes it—leaving only the formal essence of behaviour.
This is why Eventz works.
This is why it is too simple to fail.