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.”
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.
Does Eric read his comments?
Yes, I do.
And .....
I lovingly crafted this email on a vintage Ububtu 24.04 Machine
"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.
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.