describes the Curry-Howard Correspondence, a fundamental concept where logical propositions map to types and proofs map to programs (lambda terms) of those types.
I like the question → answer → proof ladder. It makes explicit something that often stays implicit: what kind of thing a program fundamentally is.
One nuance I’d add is that in denotational systems, the question already lives in a space where meaning is well-defined. Running it doesn’t construct meaning so much as reveal it. The “answer” is a value in the same semantic domain, not a byproduct of execution history.
That’s where I see the key distinction you’re pointing at:
Interrogative / Denotational: meaning-first, compositional, reasoning is local
Constructive / Operational: proof-by-execution, stateful, reasoning is global
Curry–Howard fits beautifully here, but it also highlights the danger: once proofs become operational artifacts, we start optimizing the proof process rather than preserving the meaning of the proposition.
The really interesting systems, I think, are the ones where the specification is already a proof, and execution is just evaluation.
Thanks for pushing this axis forward — it’s a much clearer lens than “declarative vs imperative.”
So let me naively ask this question. Is the argument being made by Mr. Elliott et al that β-reduction is imperative as you reduce to a normal term?
My completely naive and wrong take is that Plotkin observed some issues of program equivalence with the mathematical model of Denotational Semantics, and that context is not pertaining to a declarative versus imperative programming framing or taxonomy.
Continuing with the naivety, I would argue that Lambda Calculus and Functional Programming have both an Aristotelian Theoretical Reasoning (Proofs) and Procedural Reasoning (β-reduction) nature, and Operational Semantics provides a perspective of the balance of the two but is still within the domain of functional or "declarative" programming. Operational Semantics is not by definition "imperative programming". β-reduction yes. Imperative programming by definition no.
Your framing of Actions as time entanglement and pure functions as calculations comes to mind. Functional or declarative programming does not eliminate actions instead it has conventions for mitigating actions/time. Maybe Plotkin is just reminding us that like day and night, functional programming is both referential transparency AND time mitigation. Or, functional programming is both Theoretical Reasoning and β-reduction aka Procedural Reasoning.
I know .. I sound like Jacques Derrida :-). There is no outside text. :-)
Functional Programming is Denotational Semantics with differing eternally unstable Operational Semantics :-) :-) :-)
OK. Fun stuff. I know I am a rank amateur and all wet.
Had a chance to think about this. Here is naive take number 2.
Yes, the PLT community has different mathematical approaches to program equivalence (denotational and operational semantics), and yes these approaches address other concerns (addressing Lambda Calculus foundational properties, etc).
But maybe that is not the best context for evaluating "imperative" v "declarative" styles. :-).
But if we back up from PLT and consider the meta framework for reasoning:
- Theoretical reasoning (truthy derivation)
- Practical reasoning (being .. breakdown ... reasoning about action)
- Productive reasoning (step 1, step 2, step 3)
And given "computation"
- symbol -> transition - symbol`
- term -> reduction - term`
I would naively argue that all computation is "productive" with a "theoretical" engine. it is both.
Therefore the difference between "imperative" and "functional" style is which side do you lean towards the most.
So, here are two naive definitions
- The "imperative" mental model is "chronological steps"
- The "declarative" mental model is "expression reduction" (whether small step or large step).
Both machine and language models of computation have control flow at some level of abstraction and hence the first. Both the machine and language model have "truthy" derivation somewhere in the implementation.
Nota Bene: I naively look at small step evaluation as timeless "expression reduction" of symbols that include symbols for the environment and store :-). It is math correct? :-)
Yes, I believe you are right. They're both mechanical. The real difference is in the mechanism.
> - The "imperative" mental model is "chronological steps"
> - The "declarative" mental model is "expression reduction" (whether small step or large step).
You've nailed it. Denotational semantics define the meaning of an expression as the combination of the meanings of its subexpressions, which is "reduction". Operational semantics define the meaning of an expression as some operation (read/update) on the current state of the machine, hence "chronological steps".
Eric — this really resonated. Your critique of “declarative” as a vibe dependent on the reader’s ignorance is spot-on. Reframing the axis as denotational vs operational finally makes the distinction objective and reason-able.
What struck me most was the connection to runnable specifications. Once meaning is explicit and compositional, execution becomes secondary — almost an implementation detail. That separation (or collapse) of specification and implementation feels like the real senior-level skill you’re pointing at.
I’ve been exploring this same distinction at the system level, not just the function level: treating an entire system as a denotation where new meaning is derived from prior meaning plus an event, rather than as an operational choreography of services and state. When semantics are explicit, reasoning becomes local again — even across time.
Your post helped me put the right words on that intuition. Thanks for articulating it so clearly.
"You want to write down a question and run it to get the answer."
It seems like the appropriate designation should derive from this statement.
Question: Interrogative <- Denotational <- Declarative
Answer: This implies a form of proof...
Proof: Constructive <- Operational <- Imperative
"A proof is a program",
describes the Curry-Howard Correspondence, a fundamental concept where logical propositions map to types and proofs map to programs (lambda terms) of those types.
Fred — this is a very sharp framing.
I like the question → answer → proof ladder. It makes explicit something that often stays implicit: what kind of thing a program fundamentally is.
One nuance I’d add is that in denotational systems, the question already lives in a space where meaning is well-defined. Running it doesn’t construct meaning so much as reveal it. The “answer” is a value in the same semantic domain, not a byproduct of execution history.
That’s where I see the key distinction you’re pointing at:
Interrogative / Denotational: meaning-first, compositional, reasoning is local
Constructive / Operational: proof-by-execution, stateful, reasoning is global
Curry–Howard fits beautifully here, but it also highlights the danger: once proofs become operational artifacts, we start optimizing the proof process rather than preserving the meaning of the proposition.
The really interesting systems, I think, are the ones where the specification is already a proof, and execution is just evaluation.
Thanks for pushing this axis forward — it’s a much clearer lens than “declarative vs imperative.”
When naming things sometimes the best name is based on the reason why the thing exists: screwdriver, apple-peeler, etc.
I believe this notion aligns with your "really interesting systems" wherein the specification is already a proof.
Hello Eric. First of all, I want to thank you for all of your work on FP including Grokking Simplicity. I personally found it amazingly helpful.
Now, for other reasons before I saw this article, I went down the rabbit hole of reading Plotkin's "LCF Considered as a Programming Language" (https://homepages.inf.ed.ac.uk/gdp/publications/LCF.pdf) and "A Structural Approach to Operational Semantics" (https://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf).
So let me naively ask this question. Is the argument being made by Mr. Elliott et al that β-reduction is imperative as you reduce to a normal term?
My completely naive and wrong take is that Plotkin observed some issues of program equivalence with the mathematical model of Denotational Semantics, and that context is not pertaining to a declarative versus imperative programming framing or taxonomy.
Continuing with the naivety, I would argue that Lambda Calculus and Functional Programming have both an Aristotelian Theoretical Reasoning (Proofs) and Procedural Reasoning (β-reduction) nature, and Operational Semantics provides a perspective of the balance of the two but is still within the domain of functional or "declarative" programming. Operational Semantics is not by definition "imperative programming". β-reduction yes. Imperative programming by definition no.
Your framing of Actions as time entanglement and pure functions as calculations comes to mind. Functional or declarative programming does not eliminate actions instead it has conventions for mitigating actions/time. Maybe Plotkin is just reminding us that like day and night, functional programming is both referential transparency AND time mitigation. Or, functional programming is both Theoretical Reasoning and β-reduction aka Procedural Reasoning.
I know .. I sound like Jacques Derrida :-). There is no outside text. :-)
Functional Programming is Denotational Semantics with differing eternally unstable Operational Semantics :-) :-) :-)
OK. Fun stuff. I know I am a rank amateur and all wet.
Peace
Had a chance to think about this. Here is naive take number 2.
Yes, the PLT community has different mathematical approaches to program equivalence (denotational and operational semantics), and yes these approaches address other concerns (addressing Lambda Calculus foundational properties, etc).
But maybe that is not the best context for evaluating "imperative" v "declarative" styles. :-).
But if we back up from PLT and consider the meta framework for reasoning:
- Theoretical reasoning (truthy derivation)
- Practical reasoning (being .. breakdown ... reasoning about action)
- Productive reasoning (step 1, step 2, step 3)
And given "computation"
- symbol -> transition - symbol`
- term -> reduction - term`
I would naively argue that all computation is "productive" with a "theoretical" engine. it is both.
Therefore the difference between "imperative" and "functional" style is which side do you lean towards the most.
So, here are two naive definitions
- The "imperative" mental model is "chronological steps"
- The "declarative" mental model is "expression reduction" (whether small step or large step).
Both machine and language models of computation have control flow at some level of abstraction and hence the first. Both the machine and language model have "truthy" derivation somewhere in the implementation.
Nota Bene: I naively look at small step evaluation as timeless "expression reduction" of symbols that include symbols for the environment and store :-). It is math correct? :-)
Ok
Peace
Yes, I believe you are right. They're both mechanical. The real difference is in the mechanism.
> - The "imperative" mental model is "chronological steps"
> - The "declarative" mental model is "expression reduction" (whether small step or large step).
You've nailed it. Denotational semantics define the meaning of an expression as the combination of the meanings of its subexpressions, which is "reduction". Operational semantics define the meaning of an expression as some operation (read/update) on the current state of the machine, hence "chronological steps".
Does Eric read his comments?
Yes, I do.
And .....
I lovingly crafted this email on a vintage Ububtu 24.04 Machine
denotive
Eric — this really resonated. Your critique of “declarative” as a vibe dependent on the reader’s ignorance is spot-on. Reframing the axis as denotational vs operational finally makes the distinction objective and reason-able.
What struck me most was the connection to runnable specifications. Once meaning is explicit and compositional, execution becomes secondary — almost an implementation detail. That separation (or collapse) of specification and implementation feels like the real senior-level skill you’re pointing at.
I’ve been exploring this same distinction at the system level, not just the function level: treating an entire system as a denotation where new meaning is derived from prior meaning plus an event, rather than as an operational choreography of services and state. When semantics are explicit, reasoning becomes local again — even across time.
Your post helped me put the right words on that intuition. Thanks for articulating it so clearly.