\section{Expressiveness, Verifiability, Tractability}

\subsection{The EVT Hypothesis}

We state the main conjecture below.

\begin{conj}[{Expressiveness/Verifiability/Tractability (``EVT'') Hypothesis}\label{EVT}]
The conjecture formally comprises two parts:
\begin{enumerate}[label=(\Alph*)]
    \item \textbf{Loss of Global Verifiability in Macro-expressive Systems.} As the expressive power of a system of physical computation increases, the range of its globally algorithmically verifiable behaviors generally decreases unless additional structural restrictions are imposed.

    \item \textbf{Expressiveness/Verifiability/Tractability Trilemma.} Within such a system, every deterministic computational model is fundamentally constrained by a three-way tradeoff among \emph{expressiveness} (geometric or semantic generality), \emph{verifiability} (algebraic checkability or formal runtime assurance), and \emph{tractability} (algorithmic or computational efficiency). These attributes satisfy the following trilemma:

    \medskip

    \emph{\textbf{No system can simultaneously maximize all three properties.} For any given model, at most two of the three can be optimized beyond a critical threshold, while the third must necessarily be sacrificed.}
\end{enumerate}
\end{conj}

A selection principle and conservation law for computational behavior. First mentioned in the context of topological gauge theories in \cite{Kaminsky2025Geocomp}.\footnote{``Professor, why is the Python code running slowly?'' ``Aha, well you see, the geometry of a Yang--Mills field is such that there are these computational helices and uh...''} For readers more comfortable with physical language, the trilemma can be re-expressed in standard thermodynamic language. These are \emph{not} physical laws; they are organizing claims about structural limits induced by computability, complexity, and the interaction costs of programming and proof.  Each law should be read relative to the definitions already fixed: macro-expressiveness (\cref{sec:expressiveness}), type-based verifiability (\cref{sec:verifiability}), and polynomial-overhead tractability (\cref{sec:tractability}).

\begin{conj}[The First Law of Programming Thermodynamics]
\label{conj:first-law}
There exists a theoretical upper boundary in the feasible region of language designs: beyond that boundary, no language can simultaneously increase expressiveness and verifiability \emph{while retaining} (a) soundness of its verification discipline, (b) compiler/pipeline tractability, and (c) human comprehensibility.
\end{conj}

\paragraph{Interpretation.}
The First Law is a geometric restatement of the \textsc{EVT} trilemma already discussed: if we view ``language designs'' as points in a space parameterized by (at least) expressiveness $E$, verifiability $V$, and tractability $T$, then the set of \emph{viable} points is not all of $\mathbb{R}^3$ but a constrained region.
The claim is that this region has a \emph{nontrivial boundary}: pushing a design past it forces at least one of the three guardrails to fail.

\paragraph{Operational reading.}
Attempts to build a ``maximal'' language (high $E$ and high $V$) tend to fail in recognizable ways:
\begin{enumerate}[label=(F\arabic*), leftmargin=3.2em]
  \item \textbf{Consistency failure.} The static discipline becomes unsound (the verifier certifies false semantic claims).
  \item \textbf{Compilability failure.} Elaboration/typechecking/evaluation incur uncontrolled blowups (super-polynomial overhead, global proof search, etc.).
  \item \textbf{Comprehensibility failure.} The system becomes unusable by humans except via opaque automation, defeating the point of a programming language as an \emph{interface}.
\end{enumerate}
We treat these as distinct ``failure modes'' rather than a single generic impossibility.

\medskip

\begin{conj}[The Second Law of Programming Thermodynamics]
\label{conj:second-law}
In a sufficiently expressive regime, increasing verifiability induces an entropic loss in expressiveness, and vice versa: the tradeoff is directional and cannot, in general, be reversed without some form of external intervention (e.g.\ restricting the language, strengthening trusted automation/oracles, or importing additional proof burden).
\end{conj}

\paragraph{Interpretation.}
The Second Law asserts a \emph{directional} coupling between $E$ and $V$ once expressiveness is above a threshold where nontrivial semantic phenomena appear (effects, control, higher-order state, reflection, etc.).  In that regime, ``turning up'' verifiability typically means introducing restrictions, annotations, or proof obligations that reduce what can be expressed \emph{directly} (macro-expressiveness), or at least reduce what can be expressed \emph{tractably}.

\paragraph{A minimal formal reading.}
Fix a baseline core $L_{\mathsf{core}}$ and consider a family of surface languages $\{L_\alpha\}$ that share the same core evaluation model but differ by (a) added expressive facilities and (b) verification discipline. The Second Law can be read as the claim that, in such families, there is a persistent monotonic tension:
\[
\Delta V > 0 \quad\Rightarrow\quad \Delta E < 0 \ \ \text{or}\ \ \Delta T < 0,
\]
and dually for $\Delta E>0$.
Here ``entropic'' is shorthand for the observation that once global semantic power is admitted, restoring strong verification typically requires adding structure (types/proofs/constraints) whose management creates irreversible overhead: proof artifacts accumulate, inference requires human guidance, or compilation must perform whole-program reasoning.

\paragraph{``Irreversible without intervention.''}
We do \emph{not} mean that language evolution is literally irreversible, but that there is no general-purpose, purely local refactoring that simultaneously restores lost verifiability \emph{and} retains full expressiveness at the same tractability level. Something must give:
\begin{itemize}[leftmargin=2.2em]
  \item restrict the language (e.g.\ to total/terminating fragments),
  \item accept larger proof/certificate burdens,
  \item rely on stronger trusted automation (SMT, proof search, certified compilers),
  \item or weaken the property being verified.
\end{itemize}
This parallels the way CAP is used as an analogy: the adversary (semantic power, undecidability, interaction cost) forces a directional compromise.

\medskip

\begin{conj}[The Third Law of Programming Thermodynamics]
\label{conj:third-law}
As verifiability approaches its theoretical maximum, expressiveness must approach triviality (e.g., \ total or strongly normalizing languages, or systems whose observational theory is decidable).  However, no nondegenerate system of computation can reach zero expressive power.
\end{conj}

\paragraph{Interpretation.}
The Third Law isolates an ``absolute zero'' phenomenon: maximal verifiability---understood as a regime where semantic reasoning becomes uniformly decidable, proof obligations are bounded, and equivalence is mechanically tame---forces the language toward a class with sharply limited behaviors.  In practice, this often means some combination of:
\begin{itemize}[leftmargin=2.2em]
  \item \textbf{termination by design} (total functional programming/normalization-based proof assistants),
  \item \textbf{restricted effects/control} (to preserve decidable checking and tractable reasoning),
  \item \textbf{finite-state/decidable observational theories} (so verification is complete for a rich class of properties).
\end{itemize}

\paragraph{Why ``triviality'' is the limit ``zero expressiveness'' is unattainable.}
If we idealize ``maximal verifiability'' as demanding that a large class of semantic questions (including nontrivial equivalences or refinement checks) be decidable and compositional, then classical undecidability pressures force severe restrictions on behavior.  Totality/strong normalization is one principled route: it makes definitional equality and proof checking tractable, but it also excludes many expressive phenomena that rely on general recursion or unrestricted effects.

A system with \emph{literally} zero expressive power would admit no meaningful behavioral distinctions at all; its programs would collapse (up to contextual equivalence) into a single observational class or a finite set of trivial observations. Such a ``language'' is better viewed as a degenerate logic (e.g.\ a fragment whose evaluation is vacuous), not as a programming language.  The Third Law, therefore, says: even in the limit where $V$ is pushed as high as possible, a viable system must retain some minimal degree of behavioral variation (at least enough to encode nontrivial propositions, data, or transformations), hence it cannot collapse to absolute expressive nullity. 

\medskip

The trilemma provides the local obstruction: in any sufficiently rich regime, one cannot maximize all desiderata simultaneously. The ``laws'' are a global packaging:
\begin{itemize}[leftmargin=2.2em]
  \item the First Law asserts an upper boundary in the design space (a feasible region with edges),
  \item the Second Law asserts directionality of the $E$--$V$ tension in expressive regimes,
  \item the Third Law identifies the limiting behavior as $V$ approaches its maximum.
\end{itemize}
None of these claims requires us to commit yet to a unique numeric definition of $E, V, T$; they only require that our comparison notions behave monotonically under the standard moves of language design (adding primitives, restricting syntax/semantics, strengthening static disciplines, and shifting burden between the programmer and the machine).

\subsection{Expressiveness}
\label{sec:expressiveness}

What is ``expressive power''? 

\medskip

If we only ask which \emph{functions} a language can compute, then (barring restrictions such as totality or strong normalization) most real languages collapse into the same equivalence class: they are universal. But programmers do not experience languages as mere function algebras. They experience \emph{abstraction mechanisms}: binding forms, modules, control operators, effects, type disciplines, and the accompanying equational laws and reasoning principles. Expressiveness, in the sense relevant to language design, is about which abstractions can be provided \emph{as primitives} versus which can be treated as \emph{definitional} (``syntactic sugar'') without disturbing the semantic fabric of the language.

\medskip

The modern starting point for making this precise is Felleisen's program: compare languages not by the set of computable functions, but by the existence (or non-existence) of \emph{structure-preserving eliminations} of proposed features \cite{Felleisen1991ExpressivePower}. Informally, an extension is ``inessential'' if it can be compiled away by a local, syntax-directed translation that preserves the observable behavior of programs. This section sets up a framework that makes our \emph{micro-} vs.\ \emph{macro-} expressiveness distinction precise and robust enough to support later arguments about \textsc{EVT} tradeoffs.

\medskip

Fix a \emph{language universe} $\mathcal{L}$: a set of term-formers (constructors) together with a notion of \emph{program} and an operational semantics. Concretely, one may think of $\mathcal{L}$ as a grammar of expressions $e$ built from a signature $\Sigma_{\mathcal{L}}$ together with:
\begin{itemize}[leftmargin=2.2em]
  \item a subset $\mathrm{Prog}(\mathcal{L})$ of \emph{closed} expressions designated as programs;
  \item a reduction relation $\to_{\mathcal{L}}$ (small-step) and/or an evaluation judgment $e \Downarrow_{\mathcal{L}} v$ (big-step);
  \item a set of observable outcomes $\mathrm{Obs}$ (e.g.\ termination with a value, raising an exception, producing an I/O trace, divergence).
\end{itemize}
A \emph{sublanguage} $L \preceq \mathcal{L}$ is obtained by restricting $\Sigma_{\mathcal{L}}$ to a subsignature $\Sigma_L \subseteq \Sigma_{\mathcal{L}}$ and inheriting the induced semantics on those terms.

\begin{defn}[Conservative restriction/extension]
\label{def:conservative}
Let $L \preceq \mathcal{L}$ be a sublanguage. A further restriction $L_0 \preceq L$ is a \emph{conservative restriction} if every $L_0$-program has the same observable behavior when evaluated in $L_0$ as when evaluated in $L$ (i.e.\ the added constructs of $L$ do not change the meaning of programs that do not use them). Dually, $L$ is a \emph{conservative extension} of $L_0$ when $L_0 \preceq L$ and $L_0$ is a conservative restriction of $L$.
\end{defn}

Conservativity is the minimum sanity condition needed to discuss whether ``new'' constructs add expressiveness: we do not want an extension to count as ``more expressive'' merely because it changes the semantics of the old language. To compare programs, we need a notion of observability. The most common choice is contextual observation: two terms are equivalent if no program context can tell them apart.

\begin{defn}[Program contexts and contextual equivalence]
\label{def:contextual-equivalence}
A \emph{program context} $C[\cdot]$ for a language $L$ is an $L$-expression with a single hole such that, whenever $e$ is an $L$-expression of the appropriate syntactic category, $C[e]$ is an $L$-program.
We write $\mathrm{Ctx}(L)$ for the set of program contexts of $L$.

Fix an observation function $\mathrm{Obs}_L : \mathrm{Prog}(L) \to \mathrm{Obs}$ (e.g.\ $\mathrm{Obs}$ could distinguish termination-with-value from divergence, or could record traces).
Two $L$-expressions $e,e'$ are \emph{contextually equivalent}, written $e \approx_L e'$, if
\[
\forall C[\cdot]\in \mathrm{Ctx}(L),\quad \mathrm{Obs}_L(C[e]) = \mathrm{Obs}_L(C[e']).
\]
\end{defn}

Note that
\begin{itemize}[leftmargin=2.2em]
  \item The choice of $\mathrm{Obs}$ matters (may-termination vs.\ must-termination, trace equivalence, etc.). For the \textsc{EVT} story, we only need that $\approx_L$ is a congruence induced by contexts, and that it matches the intended notion of ``same behavior'' for the paper's examples.
  \item If one prefers, $\approx_L$ can be defined using a labeled transition system and trace sets; the development below still goes through.
\end{itemize}

\paragraph{Eliminability and translations.} We now formalize what it means for an extension to be ``just sugar.'' The key is to restrict the set of admissible translations. Let $L = L_0 + \{F_i\}_{i\in I}$ be a conservative extension of $L_0$ inside some universe $\mathcal{L}$, where the $F_i$ are the \emph{additional} constructors (facilities) not present in $L_0$.

\begin{defn}[Eliminating translation]
\label{def:eliminating-translation}
An \emph{eliminating translation} from $L$ to $L_0$ is a function
\[
\phi : \mathrm{Expr}(L) \to \mathrm{Expr}(L_0)
\]
satisfying the following conditions.
\begin{enumerate}[label=(E\arabic*), leftmargin=3.2em]
  \item \textbf{Identity on the base.} $\phi$ is homomorphic for all constructors of $L_0$ (equivalently: it commutes with the formation rules of $L_0$), and on variables it acts as identity.
  \item \textbf{Program preservation.} If $P \in \mathrm{Prog}(L)$ then $\phi(P)\in \mathrm{Prog}(L_0)$.
  \item \textbf{Semantic preservation (adequacy).} For all programs $P\in \mathrm{Prog}(L)$,
  \[
  \mathrm{Obs}_L(P) = \mathrm{Obs}_{L_0}(\phi(P)).
  \]
\end{enumerate}
If such a $\phi$ exists, we say that the additional facilities $\{F_i\}_{i\in I}$ are \emph{eliminable} (or \emph{expressible}) in $L_0$ (with respect to $L$).
\end{defn}

This notion is intentionally permissive: an eliminating compiler could, in principle, perform global rewrites that radically change term structure, as long as it preserves observable behavior.

\paragraph{Macro-eliminability (structure-preserving eliminations).}
Felleisen's key refinement is to capture the Landin intuition of \emph{local} eliminations: translations that remove constructs \emph{compositionally}, without inspecting whole-program structure. This matches how programmers and implementers actually treat ``inessential'' language features: they compile away by macro-expansion or fixed desugaring schemas \cite{Felleisen1991ExpressivePower}.

\begin{defn}[Syntactic abstractions]
\label{def:syntactic-abstraction}
A (multi-hole) \emph{syntactic abstraction} over $L_0$ is a context-like term former
\[
A(\cdot_1,\ldots,\cdot_k)
\]
built from the constructors of $L_0$ with $k$ holes, such that plugging in $k$ expressions of the right categories yields an $L_0$-expression.
\end{defn}

\begin{defn}[Macro-eliminability/macro-expressibility]
\label{def:macro-eliminability}
Let $L = L_0 + \{F_i\}_{i\in I}$ be a conservative extension. The added facilities are \emph{macro-eliminable} if there exists an eliminating translation $\phi : L \to L_0$ such that, for each $a$-ary constructor $F \in \{F_i\}_{i\in I}$, there is a fixed $a$-ary syntactic abstraction $A_F$ over $L_0$ with
\[
\phi\bigl(F(e_1,\ldots,e_a)\bigr) \;=\; A_F\bigl(\phi(e_1),\ldots,\phi(e_a)\bigr)
\quad\text{for all } e_1,\ldots,e_a.
\]
In this case we also say: \emph{$L_0$ can macro-express the facilities $\{F_i\}$ (with respect to $L$)}.
\end{defn}

Intuitively: each new construct $F$ has a \emph{single} expansion schema $A_F$ that expresses it using only $L_0$-constructs, and the translation of a compound phrase is obtained by composing the translations of its subphrases.

\paragraph{Micro- vs.\ macro-expressiveness} The micro/macro distinction can now be aligned to the above.

\begin{defn}[Micro-expression (inessential extension)]
\label{def:micro-expression}
A conservative extension $L = L_0 + \{F_i\}_{i\in I}$ is \emph{micro-expressive} (relative to $L_0$, within $\mathcal{L}$) if the added facilities are macro-eliminable in the sense of \cref{def:macro-eliminability}. Equivalently: the extension admits a structure-preserving, local desugaring into $L_0$ that preserves program observations.
\end{defn}

\begin{defn}[Macro-expression (essential extension)]
\label{def:macro-expression}
A conservative extension $L = L_0 + \{F_i\}_{i\in I}$ is \emph{macro-expressive} (relative to $L_0$, within $\mathcal{L}$) if the added facilities are \emph{not} macro-eliminable; i.e.\ there exists at least one added constructor $F$ for which no semantics-preserving elimination can be given by a fixed syntactic abstraction schema over $L_0$.
\end{defn}

Without restricting translations, almost any feature can be simulated by a sufficiently global compilation strategy (CPS conversion, whole-program defunctionalization, staging, proof-carrying code, etc.). Macro-eliminability is a principled way to prevent the comparison from collapsing, by requiring eliminations to be \emph{local} and \emph{structure-preserving} \cite{Felleisen1991ExpressivePower}. This makes expressiveness claims reflect what language users typically mean: whether a feature can be provided as mere notation and library code without changing the underlying reasoning principles.

\paragraph{Examples and non-examples.}
The following examples calibrate the definitions. They are illustrative; later sections will pick a stable ``reference universe'' tailored to the EVT argument.

\begin{ex}[A canonical micro-expressive extension: \texttt{let}]
In a call-by-value $\lambda$-calculus with functions, a \texttt{let}-binding is macro-eliminable by the standard desugaring
\[
\phi(\texttt{let } x = v \texttt{ in } e) \;=\; (\lambda x.\phi(e))\,\phi(v),
\]
with $\phi$ otherwise homomorphic. This is exactly Landin's paradigm of ``inessential'' constructs: a local compilation rule that preserves behavior.
\end{ex}

\begin{ex}[A canonical ``global'' translation: CPS is not a macro translation]
Continuation-passing style conversion provides a semantics-preserving translation from direct style into a continuation language, and conversely (under hypotheses) an inverse mapping. But CPS is a \emph{whole-program} restructuring: it changes the shape of essentially every subterm, threads an extra continuation argument throughout, and typically requires global administrative reductions. Sabry and Felleisen's analysis of CPS reasoning highlights exactly this phenomenon: CPS-equivalent programs admit reasoning principles that are not available in the original direct-style calculus without additional axioms \cite{SabryFelleisen1993CPS}. In our terminology, CPS exemplifies a powerful eliminating translation that is \emph{not} macro-eliminability evidence.
\end{ex}

\begin{ex}[Expressible but not macro-expressible: polymorphic \texttt{let} (phenomenon)]
One of Felleisen's motivations for macro-expressiveness is that a feature may be eliminable in a permissive sense while failing to admit a local, structure-preserving elimination. A classic instance is that polymorphic \texttt{let} can be simulated in some monomorphic settings by global transformations, yet does not satisfy the macro-eliminability criterion in the relevant framework. This gap between ``there exists an encoding'' and ``there exists a macro-expansion'' is exactly what micro- vs.\ macro-expressiveness is meant to track.
\end{ex}

\paragraph{Relative expressiveness as a preorder.} Macro-eliminability yields a comparative relation between sublanguages inside a fixed universe.

\begin{defn}[Relative (macro-)expressiveness]
\label{def:relative-expressiveness}
Let $L_0$ and $L_1$ be conservative restrictions of a common universe $\mathcal{L}$.
We say that $L_1$ is \emph{at least as macro-expressive as} $L_0$ (with respect to $\mathcal{L}$), and write
\[
L_0 \preceq_{\mathrm{macro}} L_1,
\]
if whenever $L_0$ contains (or can macro-express) a set of additional $\mathcal{L}$-facilities, then $L_1$ also contains (or can macro-express) those facilities.
\end{defn}

\begin{prop}
\label{prop:preorder}
$\preceq_{\mathrm{macro}}$ is a preorder on conservative restrictions of a fixed universe $\mathcal{L}$ (reflexive and transitive).
\end{prop}

\begin{proof}[Proof sketch]
Reflexivity is immediate. Transitivity follows by composition of macro-eliminations: if $L_2$ macro-expresses what $L_1$ can macro-express, and $L_1$ macro-expresses what $L_0$ can macro-express, then $L_2$ macro-expresses what $L_0$ can macro-express. The technical point is that macro-eliminations compose because each eliminated construct is replaced by a fixed syntactic abstraction schema, hence the composite remains syntax-directed.
\end{proof}

The payoff of such definitions is that expressiveness becomes something we can \emph{reason about} structurally:
\begin{itemize}[leftmargin=2.2em]
  \item Micro-expressive extensions preserve the ``semantic laws'' of the core: they do not introduce fundamentally new observation principles, merely new surface forms.
  \item Macro-expressive extensions tend to invalidate or refine existing laws: new distinctions appear, new equivalences break, and reasoning about old code may require stronger semantic models or proof obligations \cite{Felleisen1991ExpressivePower}.
\end{itemize}
This ``law invalidation'' perspective is the bridge to \textsc{EVT}: increasing expressiveness is not free, because it changes what must be tracked to verify programs, and it changes which transformations remain sound.

\subsection{Verifiability}
\label{sec:verifiability}

What is \emph{verifiability}? 

\medskip

Informally, it is the extent to which a language admits \emph{effective, scalable methods} for establishing semantic properties of programs \emph{before} they run. This includes safety properties (``does not go wrong''), representation invariants, effect-discipline claims (``no mutation occurs here''), and richer functional correctness assertions. The \textsc{EVT} perspective treats verifiability as a first-class design axis: languages are not just devices for \emph{expressing} computations, but also for \emph{proving} facts about those computations.

\medskip

A first obstacle is that most interesting semantic properties of programs are not decidable in full generality. Thus, verifiability in practice almost always proceeds by (a) restricting the property language, (b) restricting the program language, or (c) accepting incomplete methods (semi-decision procedures, bounded model checking, interactive proofs, etc.). Type systems are the canonical instance of option (a): they provide a compositional, syntax-directed proof discipline whose judgments can usually be checked mechanically and locally. Pierce’s presentation of type systems is particularly useful here because it isolates what we need for the EVT: a clean separation between \emph{static semantics} (judgments and proofs) and \emph{dynamic semantics} (evaluation), linked by a \emph{soundness theorem} \cite{Pierce2002TAPL}.

\medskip

To speak precisely, we model verification as a relation between programs and specifications.

\begin{defn}[Specifications and satisfaction]
Fix a language $L$ with programs $\mathrm{Prog}(L)$ and an observation map $\mathrm{Obs}_L : \mathrm{Prog}(L)\to \mathrm{Obs}$ (as in \cref{def:contextual-equivalence}). A \emph{specification} is an element $\varphi$ of some specification class $\Phi$ equipped with a satisfaction relation
\[
P \models_L \varphi.
\]
For example, $\varphi$ may assert safety (no stuck states), termination, trace constraints, noninterference, or refinement of an abstract model.
\end{defn}

\begin{defn}[Verifier, soundness, completeness]
A (mechanical) \emph{verifier} for $(L,\Phi)$ is a partial procedure
\[
\mathcal{V} : \mathrm{Prog}(L)\times \Phi \rightharpoonup \{\mathsf{yes},\mathsf{no}\}.
\]
It is \emph{sound} if whenever $\mathcal{V}(P,\varphi)=\mathsf{yes}$, we have $P\models_L \varphi$.
It is \emph{complete} if whenever $P\models_L \varphi$, we have $\mathcal{V}(P,\varphi)=\mathsf{yes}$.
\end{defn}

In realistic settings, completeness is often too strong: we may settle for semi-decision procedures, or for soundness with false negatives, or for a proof-producing verifier that may require user guidance.

\paragraph{Types as lightweight program logics.} Type systems instantiate verification by letting \emph{types} themselves play the role of specifications. In the standard account (Pierce), a type system consists of a typing relation $\Gamma \vdash e : \tau$ together with an operational semantics for evaluation \cite{Pierce2002TAPL}. The intended reading is:
\[
\Gamma \vdash e : \tau
\quad\Rightarrow\quad
\text{``under assumptions $\Gamma$, $e$ behaves like a $\tau$-thing.''}
\]
What ``behaves like'' means depends on the semantics and the chosen notion of observation, but the central guarantee is \emph{type safety}.

\begin{defn}[Type safety via progress and preservation (schema)]
Let $L$ be a language with expressions $e$, values $v$, and evaluation step $e\to e'$.
A type system for $L$ is \emph{type safe} if it satisfies:
\begin{enumerate}[label=(TS\arabic*), leftmargin=3.2em]
  \item \textbf{Preservation.} If $\Gamma \vdash e:\tau$ and $e\to e'$, then $\Gamma \vdash e':\tau$.
  \item \textbf{Progress.} If $\varnothing \vdash e:\tau$ (closed well-typed term), then either $e$ is a value or there exists $e'$ with $e\to e'$.
\end{enumerate}
\end{defn}

This is the familiar Wright--Felleisen/Pierce pattern: well-typed programs do not get stuck, and evaluation preserves typing \cite{WrightFelleisen1994TypeSoundness, Pierce2002TAPL}. In EVT terms, the typing judgment is a proof object (often implicit) that certifies a semantic property (``will not go wrong'').

\medskip

Crucially, types are \emph{compositional} verifiers: judgments are derived by syntax-directed rules that mirror language structure. This compositionality is one of the primary reasons type systems scale: local proofs compose into global guarantees.

\paragraph{The verifiability spectrum: from inference to proof engineering.} The \emph{verifiability axis} is not binary. It ranges from fully automatic, low-friction verification to rich, proof-oriented systems with significant human effort. The tradeoff is familiar: the stronger the properties we want to express, the harder it becomes to infer, check, or construct proofs automatically.

\paragraph{Automatic regimes.}
At one end sit type disciplines designed for decidable checking and (often) decidable inference: e.g.\ Hindley--Milner style polymorphism and its descendants. The engineering aim is that the verifier is essentially invisible: a compiler elaborates implicit proofs and checks them cheaply \cite{Milner1978Polymorphism}.

\paragraph{Expressive regimes.}
Moving outward, richer type systems allow richer invariants: polymorphism with higher-rank types, refinement-like constraints, linearity/effects, etc. These systems often preserve decidable \emph{checking} but lose decidable \emph{inference}, shifting work from the machine to the programmer (annotations, proofs, solver hints).

\paragraph{Proof-carrying regimes.}
At the far end are dependent type theories, where types may quantify over values and encode full specifications. Coquand and Huet’s Calculus of Constructions is a canonical foundation: it unifies higher-order functions with a powerful dependent type discipline, enabling the Curry--Howard ``programs as proofs'' reading to become an engineering tool \cite{CoquandHuet1988CoC}. Here, the verifier is a type checker for proofs, but the proof objects may be large, and their construction may require substantial human guidance (tactics, automation frameworks, libraries). One can keep checking decidable by careful design (definitional equality via normalization), while accepting that \emph{finding} proofs or inferring types is generally not algorithmically trivial.

\medskip

From an EVT standpoint, this spectrum suggests a three-part decomposition of ``verifiability'':
\begin{enumerate}[label=(V\arabic*), leftmargin=3.2em]
  \item \textbf{Spec expressivity.} How rich is the specification language $\Phi$ (what can be stated)?
  \item \textbf{Mechanizability.} How much of the proof burden can be discharged automatically (checking vs.\ inference vs.\ synthesis)?
  \item \textbf{Cost.} What is the computational and human cost of producing and checking certificates at scale?
\end{enumerate}
We will treat these components as coupled: increasing (V1) tends to worsen (V2) or (V3), unless one restricts the underlying language, the logic, or the observation model.

\paragraph{Working definition for the EVT.} We now isolate a notion of verifiability that is strong enough for the EVT boundary statements but weak enough to encompass both lightweight and proof-carrying type systems.

\begin{defn}[Type-based verifiability (EVT working notion)]
\label{def:type-verifiability}
Let $L$ be a language and let $\mathcal{T}$ be a type system for $L$ with a judgment
\[
\Gamma \vdash_{\mathcal{T}} e : \tau
\]
whose derivations are mechanically checkable.
We say that $L$ is \emph{type-verifiable up to $\mathcal{T}$} if:
\begin{enumerate}[label=(TV\arabic*), leftmargin=3.2em]
  \item \textbf{Checkability.} There is a total algorithm $\mathrm{Check}_{\mathcal{T}}$ that decides whether a purported derivation is a valid typing derivation in $\mathcal{T}$.
  \item \textbf{Soundness-to-semantics.} There is a semantic reading $\llbracket \tau \rrbracket$ of types as specifications such that well-typed closed programs satisfy the corresponding specification (type safety is the base case) \cite{Pierce2002TAPL}.
\end{enumerate}
\end{defn}

This is intentionally minimal: it does not require inference to be decidable, nor completeness with respect to an external specification language. It captures the core ``verifiability move'': convert semantic claims into checkable static artifacts, and prove a soundness theorem linking static proofs to dynamic behavior.

\medskip

Later sections will sharpen this into the \textsc{EVT} tradeoff claims by (a) fixing specific classes of ``semantic laws'' that verifiers must preserve, and (b) distinguishing between verifiability-as-\emph{decidable classification} and verifiability-as-\emph{proof-carrying certification}. For now, the message is simple: \emph{verifiability is the ability to attach enforceable, mechanically checkable meaning to programs}, and type systems are the dominant vehicle for doing so \cite{CoquandHuet1988CoC}.

\subsection{Tractability}
\label{sec:tractability}

What does it mean for a language, semantics, or verification pipeline to be \emph{tractable}?

\medskip

Unlike expressiveness and verifiability, ``tractability'' is not usually treated as a single unified research program in programming languages. Complexity theory, as traditionally formulated, studies the intrinsic difficulty of \emph{decision problems} (e.g.\ $\mathbf{P}$ vs.\ $\mathbf{NP}$), whereas our interest is broader: the \emph{end-to-end cost} of using a language as a human tool.
In particular, a language can be Turing-complete (hence able to express computations of arbitrarily large intrinsic runtime) while still being tractable in the sense that the \emph{overhead induced by the language and its verification discipline} remains controlled.

\medskip

There \emph{is} a nearby line of work worth flagging: \emph{implicit computational complexity} (ICC) studies how language restrictions and typing/logic disciplines can \emph{guarantee} that all definable programs lie in a complexity class such as polynomial time \cite{DalLago2022ICCsurvey}. That program is relevant to the EVT as an extreme point: it achieves strong tractability by deliberately sacrificing expressiveness. Our tractability axis is weaker and more pragmatic: it measures whether the \emph{meta-processes} of elaboration, evaluation, and verification are feasible, and whether their costs are stable under realistic programming practice.

\paragraph{Tractability as pipeline cost.}

We model the use of a language as a pipeline:
\[
\text{surface program} \;\Rightarrow\text{elaboration,}{\ \ } \;
\text{core program} \;\Rightarrow\text{evaluation,}{\ \ } \;
\text{observable behavior},
\]
optionally accompanied by a proof/certificate that is checked by a verifier.
To avoid baking in a particular compiler or typechecker, we define tractability relative to an explicit choice of (a) an elaboration system, (b) a costed operational semantics, and (c) a certificate checker.

\begin{defn}[Program size]
Fix an encoding of programs as finite strings. For a program $P$, write $|P|$ for its length (or any equivalent size measure, e.g.\ AST size).
\end{defn}

\paragraph{Elaboration cost.}
Let $L_{\mathsf{surf}}$ be a surface language and $L_{\mathsf{core}}$ a conservative core calculus (often smaller, closer to evaluation).
Elaboration includes macro-expansion, desugaring, and compilation into core.

\begin{defn}[Elaboration system with cost]
\label{def:elab-cost}
An \emph{elaboration system} is a (partial) relation
\[
P \;\Downarrow^{c_{\mathsf{elab}}}\; Q
\]
where $P\in \mathrm{Prog}(L_{\mathsf{surf}})$, $Q\in \mathrm{Prog}(L_{\mathsf{core}})$, and $c_{\mathsf{elab}}\in \mathbb{N}$ is an elaboration cost.
We write $\mathrm{Elab}(P)=Q$ when the witness cost is irrelevant.
\end{defn}

Intuition: macro systems that allow small $P$ to expand into exponentially large $Q$ are \emph{elaboration-intractable} in the sense relevant to the EVT, even though they may increase expressiveness.

\paragraph{Evaluation cost.}
To speak about evaluation cost in a semantics-driven way, we use a cost semantics: a big-step relation decorated with a natural-number cost, or an equivalent small-step machine with step-count. (This is standard in the cost-semantics and resource-analysis literature \cite{DannerLicataRamyaa2015CostSemantics}.)

\begin{defn}[Costed evaluation]
\label{def:eval-cost}
A \emph{costed operational semantics} for $L_{\mathsf{core}}$ is a relation
\[
Q \;\Downarrow^{c_{\mathsf{eval}}}\; v
\]
where $Q\in \mathrm{Prog}(L_{\mathsf{core}})$, $v$ is a value (or outcome), and $c_{\mathsf{eval}}\in \mathbb{N}$ measures evaluation cost (e.g.\ number of abstract-machine steps).
\end{defn}

\paragraph{Verification cost.}
Verifiability (previous section) says that certain semantic claims can be certified by checkable artifacts.
Tractability asks: are those artifacts and their checks \emph{feasible}?

\begin{defn}[Certificates and checking cost]
\label{def:cert-cost}
Fix a specification class $\Phi$ (often induced by a type system) and a notion of certificate $\pi$.
A \emph{certificate checker} is a total procedure
\[
\mathrm{Check}(P,\varphi,\pi)\in \{\mathsf{yes},\mathsf{no}\}
\]
such that $\mathrm{Check}(P,\varphi,\pi)=\mathsf{yes}$ implies $P\models\varphi$ (soundness).
We write $c_{\mathsf{chk}}(P,\varphi,\pi)$ for the cost of running $\mathrm{Check}$ and $|\pi|$ for the size of the certificate.
\end{defn}

This schema covers:
\begin{itemize}[leftmargin=2.2em]
\item ordinary typechecking (certificate implicit; $\pi$ is a derivation tree),
\item proof-carrying code and certified resource bounds \cite{CraryWeirich2000RBC},
\item proof terms in dependent type theories (certificate explicit; checking is typically decidable, but proof construction may be expensive) \cite{CoquandHuet1988CoC}.
\end{itemize}

\paragraph{The EVT notion: polynomial overhead, not polynomial runtime.}

A key design choice: we do \emph{not} define tractability as ``all programs run in polynomial time.'' That would collapse tractability into ICC (and would make most general-purpose languages ``intractable'' by definition). Instead, we measure whether the \emph{language-induced overhead} is polynomially bounded as a function of program size.

\begin{defn}[Pipeline cost]
\label{def:pipeline-cost}
Given an elaboration system and costed evaluation as above, define the total pipeline cost for a terminating $P$ by
\[
c_{\mathsf{pipe}}(P)
\;=\;
c_{\mathsf{elab}}(P) \;+\; c_{\mathsf{eval}}(\mathrm{Elab}(P)).
\]
If verification is included for a target specification $\varphi$ with certificate $\pi$, define the verified pipeline cost by
\[
c_{\mathsf{pipe}}^{\mathsf{ver}}(P,\varphi,\pi)
\;=\;
c_{\mathsf{elab}}(P)\;+\;c_{\mathsf{chk}}(P,\varphi,\pi)\;+\;c_{\mathsf{eval}}(\mathrm{Elab}(P)),
\]
and the verified artifact size by $|P|+|\pi|+|\mathrm{Elab}(P)|$.
\end{defn}

\begin{defn}[Polynomial overhead tractability]
\label{def:poly-overhead-tractable}
A surface language $L_{\mathsf{surf}}$ (relative to a core $L_{\mathsf{core}}$ and a fixed pipeline) is \emph{tractable} if there exists a polynomial $p(\cdot)$ such that for every surface program $P$:
\begin{enumerate}[label=(T\arabic*), leftmargin=3.2em]
\item \textbf{Elaboration boundedness.} If $P \Downarrow^{c_{\mathsf{elab}}} Q$ then $c_{\mathsf{elab}} \le p(|P|)$ and $|Q|\le p(|P|)$.
\item \textbf{Checking boundedness (when applicable).} For the chosen verifiability discipline, whenever $\mathrm{Check}(P,\varphi,\pi)=\mathsf{yes}$ we have $c_{\mathsf{chk}}(P,\varphi,\pi)\le p(|P|+|\pi|)$ and (optionally, as a design desideratum) $|\pi|\le p(|P|)$.
\end{enumerate}
\end{defn}

Clause (T1) formalizes the intuition that ``burying semantics in macros'' can break tractability: if the language admits short programs whose elaborations blow up super-polynomially, then the core semantics may be simple while the surface language is not practically usable as a \emph{compositional} notation.

\paragraph{Relation to resource analysis.} There is an active PL literature on deriving machine-checkable resource bounds from high-level programs via type-based methods (automatic amortized resource analysis) and cost semantics \cite{HoffmannHofmann2010PolyPotential, HoffmannAehligHofmann2012RAML, DannerLicataRamyaa2015CostSemantics}. These works are not ``tractability of languages'' in our EVT sense, but they provide exactly the semantic technology we need: explicit cost models, compositional accounting, and checkable certificates in some regimes \cite{CraryWeirich2000RBC}. The polynomial-overhead definition captures machine-level feasibility of the pipeline. But the EVT also wants to say something about \emph{human} feasibility: whether programs and proofs are controllable without global mental backtracking. A useful bridge is to measure the structural complexity of the dependency graphs induced by a program or proof. Bounded-width graphs support efficient analyses (via dynamic programming), and they also correspond to lower ``working set'' requirements for reasoning.

\begin{defn}[Cognitive control width (CFG pathwidth proxy)]
\label{def:cognitive-width}
Let $\mathrm{CFG}(P)$ be a control-flow graph for $P$ (or for $\mathrm{Elab}(P)$) in a standard sense.
Define the \emph{cognitive control width} by
\[
\mathrm{CCW}(P) \;=\; \mathrm{pw}(\mathrm{CFG}(P)),
\]
where $\mathrm{pw}(\cdot)$ is graph pathwidth.
Optionally, for proof-carrying regimes, one can analogously define $\mathrm{CCW}_{\mathsf{proof}}(P,\pi)$ using a proof-dependency graph built from the derivation structure.
\end{defn}

Two concrete calibration facts (for context, not as axioms of the EVT):
\begin{itemize}[leftmargin=2.2em]
\item Structured (goto-free) programs have strong sparsity properties in their control-flow graphs; classic work shows bounded treewidth for broad classes of structured programs \cite{Thorup1998TreewidthCFG}.
\item More recently, control-flow graphs of structured programs have been shown to have bounded \emph{pathwidth} as a function of nesting depth, together with efficient construction of decompositions \cite{ConradoGoharshadyLam2023PathwidthCFG}.
\end{itemize}

These results justify using width as a tractability proxy: when the control (or proof) structure has bounded width, many analyses and transformations become feasible in practice, and the amount of ``global context'' required to reason locally is reduced.

\paragraph{Human-side motivation.}
On the HCI side, Green and Petre's \emph{Cognitive Dimensions of Notations} provides a vocabulary for discussing human tractability (viscosity, visibility, error-proneness, etc.) and explicitly frames usability as a space of tradeoffs rather than a single scalar \cite{GreenPetre1996CogDims}. Width parameters are not a replacement for cognitive dimensions; rather, they are one formal knob that can partially explain why some notations and control structures are easier to manipulate and analyze than others.

\paragraph{Conceptual compressibility.} Let $\approx_L$ be contextual equivalence (as in \cref{def:contextual-equivalence}).
Define the \emph{behavioral Kolmogorov complexity} of $P$ by
\[
K_{\approx}(P) \;=\; \min\{\, |Q| \;:\; Q \approx_L P \,\}.
\]
Then the ratio $K_{\approx}(P)/|P|$ informally measures redundancy/ceremony.
We will not use $K_{\approx}$ in formal theorems (it is non-computable), but it motivates the claim that ``tractability'' includes a human-facing component: how directly code reflects the essential structure of its behavior.

\subsection{Macro-expression and Rice-genericity}
\label{sec:rice-genericity}

This first clause should be read as a spectrum claim rather than as a single undecidability theorem.  The EVT Hypothesis does not assert that every increase in expressiveness immediately destroys verification, nor that Rice's theorem is the universal source of all computational opacity.  Rather, it asserts that once a computational substrate becomes sufficiently rich, global verification stops being available ``for free.''  To recover it, one must impose structure: restrict the language, restrict the dynamics, restrict the observable class, provide certificates, or accept additional proof/compilation/human burden.

\paragraph{Expressiveness and global verifiability.}
Let $E$ denote the expressive capacity of a computational system: the range of behaviors, transformations, or observables it can directly realize.  Let $V_{\mathrm{glob}}$ denote the range of global semantic properties of that system that admit uniform algorithmic verification.  The first half of the EVT Hypothesis may then be read informally as the monotonic pressure
\[
\Delta E > 0
\quad\Longrightarrow\quad
\Delta V_{\mathrm{glob}} < 0
\ \ \text{unless compensating structure is introduced.}
\]
The word ``global'' is essential.  Local verification may remain robust: type safety, conservation laws, local rewrite invariants, stabilizer fragments, syntactic safety properties, and bounded model checks can all remain available in expressive systems.  The claim concerns broad semantic properties whose verification requires understanding the system as a whole.

\paragraph{Classical symbolic endpoint: Rice-style opacity.}
In deterministic symbolic computation, the limiting case is familiar.  Once a language admits universal evaluation, effective specialization, and extensional semantic classification, Rice's theorem applies: every nontrivial extensional property of the partial function computed by a program is undecidable \cite{Rice1953Classes,Rogers1967,Soare1987}.  In this regime, macro-expressive features such as reflection, quotation/evaluation, interpreter embedding, and rich metaprogramming tend to supply the structural conditions under which self-reference and diagonalization become routine.  Verifiability is then recovered only by withdrawing some of that fuel: totality, stratification, restricted reflection, syntactic safety disciplines, or proof-carrying certificates.

\paragraph{Quantum/physical endpoint: noncommutative opacity.}
Physical computation illustrates a different endpoint.  A von Neumann machine can simulate complex-linear or noncommutative operations in software, but its native execution model is still a deterministic update over a fixed classical state representation.  Quantum computation, by contrast, has a native Hilbert-space semantics: gates are unitary transformations and observable quantities need not commute \cite{NielsenChuang2010}.  The unitary evolution of a closed quantum circuit is deterministic, but measurement produces probabilistic outcomes via the Born rule.  More importantly for EVT, incompatible observables do not admit a single global classical valuation; contextuality and noncommutativity obstruct the reduction of all behavior to one globally inspectable semantic summary \cite{KochenSpecker1967,AbramskyBrandenburger2011Contextuality}.  Here the loss of global verifiability is not primarily Rice-style self-reference, but native noncommuting composition and measurement-context dependence.

\paragraph{The common pattern.}
Rice and quantum contextuality therefore play different roles.  Rice is the symbolic/deterministic endpoint of global semantic opacity: the obstruction arises from program space, self-interpretation, and extensional classification.  Quantum computation is a physical/noncommutative endpoint: the obstruction arises from the native structure of observables and measurement.  EVT treats both as instances of a broader pattern:
\[
\text{rich composition}
\quad\Longrightarrow\quad
\text{loss of global transparent semantics}
\quad\Longrightarrow\quad
\text{verification requires additional structure.}
\]
In the symbolic case that structure may be typing, totality, stratification, or certificates.  In the quantum case it may be restriction to commuting observables, stabilizer/Clifford fragments, restricted measurement classes, error-correcting structure, or classically simulable subtheories.

\paragraph{Relation to the Second Law.}
This formulation aligns the first half of the EVT Hypothesis with the Second Law of Programming Thermodynamics.  The Second Law states that, above a threshold of semantic richness, increasing verifiability generally requires an entropic loss elsewhere: reduced expressiveness, increased proof burden, stronger automation/oracles, or degraded compilability/comprehensibility.  The present clause identifies the same phenomenon from the opposite direction: increasing expressiveness generally shrinks the class of globally verifiable behaviors unless compensating structure is added.  The ``tradeoff'' is therefore not a literal conservation equation, but a directional pressure on computational design.