\section{Modeling Expressiveness vs.\ Verifiability Tradeoffs}
\label{sec:ev-curve}

We now sketch a formal model for an expressiveness/verifiability (\textsc{E/V}) frontier. For the moment, we set aside the third axis (tractability in the broad sense, and the three-$C$ failure analysis in \cref{sec:evt-failures}) and work purely in two dimensions. The correct mathematical setting for such a discussion is therefore not $\mathbb{R}^3$ but a \emph{2D partially ordered} space of language designs.

\subsection{Computation of E and V}
\label{sec:ev-uncomputable}

It is tempting to define numerical functionals $E(L)$ and $V(L)$ directly. However, in any sufficiently rich universe of languages, both quantities are generically \emph{non-computable} in the sense that deciding them exactly would require deciding nontrivial semantic properties.

\paragraph{Expressiveness.}
Determining whether one language can simulate another, or whether a given extension is macro-expressive, ultimately depends on the semantic equivalence/translation facts of the form
\[
\exists\ \phi : L' \to L \text{ such that } \forall P,\ \mathrm{Obs}_{L'}(P)=\mathrm{Obs}_{L}(\phi(P)),
\]
and these are, in general, not decidable uniformly.
At the extreme end, asking whether a language can express all partial computable functions (``is it Turing complete?'') is itself a semantic property, and many semantic properties become undecidable once a system is universal \cite{Church1936, Turing1937}.

\paragraph{Verifiability.}
Likewise, ``can we statically prove property $\varphi$ for arbitrary programs?'' quickly collapses to halting- and Rice-style impossibility: if a static discipline were both sound and complete for a nontrivial extensional property class over a universal language, it would decide an undecidable problem.

\medskip

We do not need closed-form computation of $E(L)$ or $V(L)$ in order to state and analyze boundary phenomena. The right move is order-theoretic: define robust \emph{comparisons} ($\le$) and then reason about the shape of the feasible region.

\subsection{The E- and V-orders} \label{sec:ev-orders}

Fix a universe $\mathcal{L}$ of languages (as in \cref{sec:expressiveness}), and restrict attention to conservative sublanguages/variants of $\mathcal{L}$.

\paragraph{The expressiveness order.}
Recall $\preceq_{\mathrm{macro}}$ from \cref{def:relative-expressiveness}: it compares languages by which features they can express via structure-preserving elimination. We will write
\[
L_0 \preceq_E L_1
\quad\text{for}\quad
L_0 \preceq_{\mathrm{macro}} L_1,
\]
and interpret this as: \emph{$L_1$ is at least as expressive as $L_0$ (in the macro-expressiveness sense).}

\paragraph{The verifiability order.}
We similarly compare languages by the strength of their checkable static disciplines.
There are many reasonable ways to define this (depending on what one takes as the specification class), but we only need a monotone comparison.

\begin{defn}[Verifiability preorder]
\label{def:verifiability-preorder}
Let $L_0$ and $L_1$ be languages equipped with checkable verification disciplines $\mathcal{T}_0$ and $\mathcal{T}_1$ (type systems/certificate systems) in the sense of \Cref{def:type-verifiability}.
Write
\[
(L_0,\mathcal{T}_0)\ \preceq_V\ (L_1,\mathcal{T}_1)
\]
if every semantic guarantee certified by $\mathcal{T}_0$ (under the intended interpretation) can also be certified by $\mathcal{T}_1$ with at most polynomial blowup in certificate size and checking time.
\end{defn}

This definition is intentionally schematic: it formalizes the idea that one verifier subsumes another as a proof discipline. It avoids requiring \emph{completeness} (which is too strong in expressive settings) and focuses instead on what can be \emph{certified soundly and checkably}.

\paragraph{Numerical scales as presentations.}
If we draw an ``E/V curve'' in $[0,1]^2$, we should treat $E(L)$ and $V(L)$ as \emph{presentations} of these preorders by monotone maps into the unit interval:
\[
E: (\mathrm{Lang},\preceq_E)\to ([0,1],\le),
\qquad
V: (\mathrm{Lang},\preceq_V)\to ([0,1],\le),
\]
chosen for visualization rather than computability.
Nothing in the core argument requires $E$ and $V$ to be computable functions.

\subsection{Endpoints: Lambda-calculus as Calibration}
\label{sec:endpoints}

To anchor the discussion, we fix two well-studied endpoints: the untyped $\lambda$-calculus (ULC) and the simply typed $\lambda$-calculus (STLC). These are not claims about \emph{all} programming languages; they are calibration points inside the standard semantic universe used throughout PL theory \cite{Pierce2002TAPL}.

\paragraph{Endpoint 1: Untyped lambda calculus (ULC).}
The untyped $\lambda$-calculus is the archetypal ``pure expression machine'': it has only abstraction and application. In its standard form, it is computationally universal: it can represent all partial computable functions (Church/Turing thesis as instantiated by the Church encoding) \cite{Church1936, Turing1937, Barendregt1984Lambda}.

Concretely, ULC admits nontermination ubiquitously, e.g.
\[
\Omega \;\triangleq\; (\lambda x.\ x\,x)\ (\lambda x.\ x\,x),
\]
and no static structure in the calculus itself prevents such terms.

As an \textsc{EV} endpoint, ULC motivates the ``high $E$, low $V$'' corner:
\begin{itemize}
  \item \textbf{High expressiveness.} Universality and minimal primitives make it a convenient target for embeddings.
  \item \textbf{Low verifiability.} Without a static discipline, essentially no nontrivial semantic guarantees are derivable compositionally from the syntax alone.
\end{itemize}
In the informal $[0,1]$ picture, ULC is the prototypical point $(E,V)\approx (1,0)$.

\paragraph{Endpoint 2: Simply typed lambda calculus (STLC).}
The simply typed $\lambda$-calculus adds a static discipline (types and typing rules) that enforces a strong semantic invariant: \emph{well-typed programs do not go wrong}. More strongly, STLC is \emph{strongly normalizing}: every well-typed term terminates \cite{Tait1967SN,Girard1972SN,Pierce2002TAPL}.

This moves STLC toward the ``high $V$'' corner:
\begin{itemize}
  \item \textbf{High verifiability.} Typechecking is decidable and supports standard progress/preservation soundness theorems \cite{Pierce2002TAPL, WrightFelleisen1994TypeSoundness}.
  \item \textbf{Lower expressiveness.} The calculus is not computationally universal (no general recursion without extensions), so it cannot express all partial computable functions.
\end{itemize}
In the informal $[0,1]$ picture, STLC sits near $(E,V)\approx (0,1)$ (``low $E$, high $V$'').

\medskip

ULC and STLC demonstrate that even within the smallest plausible semantic universe, one already sees a sharp tradeoff. The goal of the EVT program is to generalize this observation from these toy calculi to the richer design space of modern languages and verification systems, and to identify the structural constraints that force the boundary.

\subsection{The E/V Frontier as a Pareto Boundary in a Poset}
\label{sec:ev-frontier}

The discussion above treats ``the $E/V$ curve'' as a visual guide. Formally, however, we will \emph{not} attempt to define computable real-valued scores $E(L),V(L)\in[0,1]$ for arbitrary languages. Instead, we model tradeoffs order-theoretically: languages are compared by preorders, and the ``boundary'' is a set of Pareto-maximal designs.

\paragraph{Language designs.}
A \emph{language design} in this section is a pair
\[
\mathbf{L} \;=\; (L,\mathcal{T}),
\]
where $L$ is a programming language (with an observation model) and $\mathcal{T}$ is a checkable verification discipline for $L$ (type system/certificate system) as in \Cref{def:type-verifiability}.

\paragraph{Expressiveness preorder.}
We write
\[
\mathbf{L}_0 \preceq_E \mathbf{L}_1
\quad:\Longleftrightarrow\quad
L_0 \preceq_{\mathrm{macro}} L_1
\]
using the macro-expressiveness preorder from \Cref{def:relative-expressiveness}.
Intuitively: $\mathbf{L}_1$ can express (via structure-preserving eliminations) at least the abstraction mechanisms available in $\mathbf{L}_0$.

\paragraph{Verifiability preorder.}
We write
\[
\mathbf{L}_0 \preceq_V \mathbf{L}_1
\]
if every semantic guarantee that can be certified in $\mathbf{L}_0$'s discipline can also be certified in $\mathbf{L}_1$'s discipline with controlled overhead.
One concrete working choice (sufficient for the EVT) is:

\begin{defn}[Verifiability subsumption (working)]
\label{def:verifiability-subsumption}
Let $\mathbf{L}_i=(L_i,\mathcal{T}_i)$ for $i\in\{0,1\}$.
Write $\mathbf{L}_0 \preceq_V \mathbf{L}_1$ if there exists a polynomial $p(\cdot)$ such that:
for every closed program $P$ of $L_0$, every specification $\varphi$ expressible/certifiable under $\mathcal{T}_0$, and every certificate $\pi$ with
\[
\mathrm{Check}_{\mathcal{T}_0}(P,\varphi,\pi)=\mathsf{yes},
\]
there exist a corresponding program $P'$ of $L_1$, specification $\varphi'$ under $\mathcal{T}_1$, and certificate $\pi'$ such that:
\[
\mathrm{Obs}_{L_0}(P)=\mathrm{Obs}_{L_1}(P'),
\qquad
\mathrm{Check}_{\mathcal{T}_1}(P',\varphi',\pi')=\mathsf{yes},
\]
and the overhead bounds hold:
\[
|P'|+|\pi'|\ \le\ p(|P|+|\pi|),
\qquad
c_{\mathsf{chk}}(P',\varphi',\pi')\ \le\ p(|P|+|\pi|).
\]
\end{defn}

\noindent
Intuitively: $\mathbf{L}_1$ can certify everything $\mathbf{L}_0$ can (up to reasonable encoding overhead), under a sound checker.

\paragraph{The product preorder and the frontier.}
We now combine the two axes into a single preorder.

\begin{defn}[$E/V$ product preorder]
\label{def:ev-product-preorder}
Define
\[
\mathbf{L}_0 \preceq_{EV} \mathbf{L}_1
\quad:\Longleftrightarrow\quad
\mathbf{L}_0 \preceq_E \mathbf{L}_1 \ \text{ and }\ \mathbf{L}_0 \preceq_V \mathbf{L}_1.
\]
Write $\mathbf{L}_0 \prec_{EV} \mathbf{L}_1$ if $\mathbf{L}_0 \preceq_{EV} \mathbf{L}_1$ and not $\mathbf{L}_1 \preceq_{EV} \mathbf{L}_0$.
\end{defn}

\begin{defn}[Pareto-maximal $E/V$ designs]
\label{def:ev-frontier-def}
Let $\mathcal{S}$ be a set of language designs (e.g.\ a family generated from a fixed core by adding features).
The \emph{$E/V$ frontier} of $\mathcal{S}$ is the set
\[
\mathrm{Frontier}_{EV}(\mathcal{S})
\;=\;
\bigl\{\mathbf{L}\in\mathcal{S}\ :\ \nexists\ \mathbf{L}'\in\mathcal{S}\ \text{with}\ \mathbf{L} \prec_{EV} \mathbf{L}'\bigr\}.
\]
\end{defn}

\begin{prop}\label{prop:frontier-antichain}If $\mathbf{L},\mathbf{L}'\in \mathrm{Frontier}_{EV}(\mathcal{S})$ are distinct, then neither $\mathbf{L}\prec_{EV}\mathbf{L}'$ nor $\mathbf{L}'\prec_{EV}\mathbf{L}$ holds. Equivalently, the strict frontier elements are pairwise incomparable under $\preceq_{EV}$.
\end{prop}

\begin{proof}
If $\mathbf{L}\prec_{EV}\mathbf{L}'$ then $\mathbf{L}$ is not Pareto-maximal by definition of the frontier, a contradiction.
\end{proof}

\paragraph{How the ``curve'' picture survives.}
The informal picture of an $E/V$ boundary is best understood as a \emph{visualization} of
$\mathrm{Frontier}_{EV}(\mathcal{S})$ under some chosen monotone coordinates (a ``chart'').
That is, one may map designs to $(x,y)\in[0,1]^2$ by any monotone summaries of $\preceq_E$ and $\preceq_V$ for the sake of exposition. But the invariant object is the frontier in the preorder, not a literal function $V=F(E)$.

\medskip

\noindent
With this in place, ULC and STLC serve as calibration points (extreme corners) inside a chosen family $\mathcal{S}$, as discussed in \Cref{sec:endpoints}.

\subsection{A Programming Language Design Space}
\label{sec:design-space-S}

The formal definition of $\mathrm{Frontier}_{EV}(\mathcal{S})$ in \Cref{def:ev-frontier-def} is only meaningful once we fix a \emph{design space} $\mathcal{S}$. If $\mathcal{S}$ were taken to be ``all languages,'' the preorder becomes too unconstrained to support clean statements. As in physics, we therefore begin with a deliberately simplified model class: a finite family of languages generated from a common core by toggling a small set of features.

\paragraph{Core calculus.}
Fix a baseline core $L_0$ (for exposition, STLC with products and unit is sufficient; see \Cref{sec:endpoints}).
We will generate variants by adding features on top of $L_0$.
This does not assert that all real languages are STLC extensions; it asserts only that STLC is a clean reference point in which $E$ and $V$ are well-understood.

\paragraph{Feature set.}
Let $\mathsf{F}$ be a finite set of feature symbols.
For concreteness, we use the following six knobs, each of which is standard in the PL literature and has well-known effects on expressiveness and verification:
\begin{align*}
\mathsf{F}\;=\;\{\;&\mathsf{rec} &&\text{(general recursion / partiality)},\\
                &\mathsf{state} &&\text{(mutable references / heap state)},\\
                &\mathsf{ctrl} &&\text{(first-class control / continuations)},\\
                &\mathsf{poly} &&\text{(parametric polymorphism)},\\
                &\mathsf{dep}  &&\text{(dependent types / propositions-as-types)},\\
                &\mathsf{refl} &&\text{(reflection / staging / metaprogramming)}\;\}.
\end{align*}

\paragraph{Feature-generated languages.}
For each subset $X \subseteq \mathsf{F}$, let $L_X$ denote ``the language obtained by extending $L_0$ with exactly the features in $X$,'' together with a specified operational semantics and observation model.
We do not need to define every $L_X$ in full detail here; it suffices that each feature corresponds to a conservative extension in the sense of \Cref{def:conservative}.

\begin{defn}[Feature lattice of language cores]
\label{def:feature-lattice}
Let
\[
\mathcal{L}_{\mathsf{F}} \;=\; \{\,L_X \mid X \subseteq \mathsf{F}\,\}.
\]
Order $\mathcal{L}_{\mathsf{F}}$ by subset inclusion on features:
\[
L_X \preceq_{\mathsf{feat}} L_Y \quad:\Longleftrightarrow\quad X \subseteq Y.
\]
\end{defn}

$(\mathcal{L}_{\mathsf{F}},\preceq_{\mathsf{feat}})$ is a finite Boolean lattice.
Joins and meets are given by union and intersection of feature sets.
We use this only as a \emph{combinatorial scaffold}: it provides a controlled space in which incomparability and multiple maximal points are unavoidable and visible.

\paragraph{Verification disciplines as part of the design.}
A language design in the EVT is not just $L_X$ but a pair $(L_X,\mathcal{T})$ where $\mathcal{T}$ is a checkable verification discipline for $L_X$ (\Cref{def:type-verifiability}).
The same core language may admit multiple verification regimes (ranging from simple type safety to rich dependent correctness). To keep the model lightweight, we parameterize verification by a small set of \emph{regimes} rather than trying to model all proof assistants.

\begin{defn}[Verification regimes]
\label{def:verification-regimes}
Let $\mathsf{R}$ be a finite set of verification regimes. For example:
\begin{itemize}
  \item $\mathsf{R}_{\mathsf{ST}}$: simple safety typing (progress/preservation).
  \item $\mathsf{R}_{\mathsf{HM}}$: inference-oriented polymorphic typing (Hindley--Milner-style).
  \item $\mathsf{R}_{\mathsf{Dep}}$: dependent typing with explicit proofs (proof-carrying).
  \item $\mathsf{R}_{\mathsf{Auto}}$: dependent typing plus significant automation/inference/search.
\end{itemize}
For each $X\subseteq \mathsf{F}$ and each $r\in\mathsf{R}$, assume a corresponding discipline $\mathcal{T}_{X,r}$ when meaningful.
\end{defn}

\begin{defn}[The controlled design space $\mathcal{S}$]
\label{def:design-space-S}
Define the design space
\[
\mathcal{S} \;=\; \{\, (L_X,\mathcal{T}_{X,r}) \mid X\subseteq \mathsf{F},\ r\in\mathsf{R},\ \mathcal{T}_{X,r}\ \text{is well-defined}\,\}.
\]
We study $\mathrm{Frontier}_{EV}(\mathcal{S})$ with respect to the preorders $\preceq_E$ and $\preceq_V$ from \Cref{sec:ev-frontier}.
\end{defn}

\paragraph{How the ``curve'' picture is recovered.}
Within $\mathcal{S}$, the Pareto frontier $\mathrm{Frontier}_{EV}(\mathcal{S})$ is typically not a single-valued function $V=F(E)$ but a set of maximal points (an antichain; \Cref{prop:frontier-antichain}).
Nevertheless, one can still draw an intuitive boundary in $(E,V)$-coordinates by:
\begin{itemize}
  \item plotting any monotone summaries (``charts'') of $\preceq_E$ and $\preceq_V$ on $[0,1]^2$, and showing the maximal points as an envelope; or
  \item restricting attention to a single \emph{design trajectory} (a chain in the lattice) and plotting the induced tradeoff along that path.
\end{itemize}
This preserves the explanatory value of the ULC/STLC endpoints while keeping the formal object of study order-theoretic.

\paragraph{Bridge to the three failure states.}
The feature-lattice model also explains why the three scenario failures in \Cref{sec:evt-failures} are not arbitrary stories. Pushing toward higher $E$ typically corresponds to adding features such as $\mathsf{rec}$, $\mathsf{state}$, $\mathsf{ctrl}$, and $\mathsf{refl}$. Pushing toward higher $V$ corresponds to strengthening regimes toward $\mathsf{R}_{\mathsf{Dep}}$ and $\mathsf{R}_{\mathsf{Auto}}$. The three failures then correspond to three ways of resolving the resulting pressure.

\begin{table}[t]
\centering
\small
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{Name (informal)} & \textbf{Features $X\subseteq\mathsf{F}$} & \textbf{Verification regime} \\
\midrule
STLC (baseline) & $\emptyset$ & $\mathsf{R}_{\mathsf{ST}}$ \\
ML-like (practical FP) & $\{\mathsf{rec},\mathsf{poly},\mathsf{state}\}$ & $\mathsf{R}_{\mathsf{HM}}$ (plus safety typing) \\
Coq/Agda-like (proof-carrying) & $\{\mathsf{dep}\}$ (often w/ inductives) & $\mathsf{R}_{\mathsf{Dep}}$ (explicit proofs) \\
Coq+automation (search-heavy) & $\{\mathsf{dep}\}$ & $\mathsf{R}_{\mathsf{Auto}}$ \\
MAXlang\texttrademark{} (toy) & $\{\mathsf{rec},\mathsf{state},\mathsf{ctrl},\mathsf{poly},\mathsf{dep},\mathsf{refl}\}$ & $\mathsf{R}_{\mathsf{Dep}}$ (no hidden search) \\
\bottomrule
\end{tabular}
\caption{A few landmark points in the controlled design space $\mathcal{S}$. These are illustrative ``coordinates'' for the reader, not a classification of real languages.}
\label{tab:landmarks}
\end{table}

\subsection{The Turing Tarpit and Real-life Programming Languages}
\label{sec:turing-tarpit}

The EVT Trilemma does not assert a conservation equality of the form ``high $E$ implies low $V$'' in all regimes. In particular, there exist computational regimes with \emph{both} low expressiveness and low verifiability. Herein lies the infamous \emph{Turing tarpit}: a setting in which ``everything is possible'' in principle (often even Turing completeness), but very little is \emph{practically} expressible or maintainable.

\medskip

The classic slogan is due to Perlis \cite{Perlis1982Epigrams}:
\begin{quote}
\emph{``Beware of the Turing tarpit in which everything is possible but nothing of interest is easy.''}
\end{quote}
The point is that a language can be universal while still being ``low $E$'' in the macro-expressiveness sense: it may lack compositional abstraction mechanisms (modules, higher-level control constructs, data abstraction, hygienic macros, etc.), so that large programs devolve into ad hoc encodings. At the same time, it can be ``low $V$'' because it provides little static structure for ruling out errors or stating invariants.

\paragraph{Examples.}
Shell scripting languages (e.g.\ \texttt{sh}/\texttt{bash}) are expressive enough to orchestrate powerful computations via external processes, but their semantics are brittle (stringly-typed data, implicit coercions, dynamic failure modes) and they offer weak static guarantees. Esoteric languages such as Malbolge occupy the extreme corner: computation is possible, but the language is intentionally hostile to human reasoning and compositional development.

The tarpit clarifies what the EVT failure modes are \emph{not}. Gödel/Tarski/Rice-style failures concern what happens when one pushes toward the upper-right boundary (high $E$ and high $V$) while trying to retain the relevant ``three C's'' constraints. Most real languages live far from that boundary: they trade away maximal verification, maximal expressiveness, or both, to remain usable and implementable. The tarpit is the opposite corner: not an advanced boundary failure, but a regime where both axes are weak and the ``theoretical universality'' is an unhelpful consolation.

The Turing tarpit reminds us that low-$E$ and low-$V$ regimes are common. The three boundary failure states (Gödel/Tarski/Rice) remind us that pushing ``up and right'' toward simultaneous high expressiveness and high verifiability encounters structural limits. The natural question is therefore: \emph{where do most real languages sit in practice?}

\medskip

\paragraph{A caveat about ``placing'' languages.}
We do not claim a canonical embedding of real languages into a numeric $[0,1]^2$ plane. Our formal object is the preorder frontier $\mathrm{Frontier}_{EV}(\mathcal{S})$ (\Cref{sec:ev-frontier}), and any picture is necessarily a \emph{chart} (a monotone summary) plus a choice of which aspects of a language one is treating as the ``language'' (core calculus vs.\ full ecosystem, standard library, tooling, and idioms). What follows is, therefore, an intentionally informal calibration for the reader.

\paragraph{High $E$, low $V$: dynamic and reflective families.}
Languages in the Lisp/Scheme lineage are often experienced as ``high expressiveness'' due to macros, reflection, and flexible evaluation models. Their static verifiability is often weaker in everyday use, either because the core is dynamically typed or because much behavior is pushed into runtime conventions.
This is not a defect; it is a deliberate choice that prioritizes rapid abstraction and metaprogramming over strong static guarantees.

\paragraph{High $V$, lower $E$: inference-oriented typed families.}
ML-style languages (and related inference-heavy typed traditions) often sit closer to the ``high verifiability'' corner: strong static typing, principled inference, and a well-developed metatheory yield robust safety guarantees with relatively low annotation burden. The corresponding cost is that certain expressive moves (unrestricted effects, reflection, highly dynamic patterns) are either discouraged, encoded indirectly, or require explicit machinery that changes the programming model.

\paragraph{Balanced regimes: systems languages under pressure.}
Many widely-used languages aim for a pragmatic middle: significant expressiveness, but with a strong enough static structure to make large systems reliable.
Rust is an explicit attempt to push verifiability upward (memory safety and aliasing discipline) without sacrificing systems-level expressiveness.
C++ sits differently: it is extremely expressive and performant, but its verifiability story often relies heavily on discipline, tooling, and conventions rather than uniform static guarantees.
Both illustrate the central EVT point: ``balance'' typically means distributing burden across language design, compiler checks, libraries, and human process rather than maximizing a single axis in isolation.

\medskip

\paragraph{Why empirical placement is future work.}
A serious, quantitative account of where languages lie would require choosing operational measures.
Even within our controlled model $\mathcal{S}$ (\Cref{sec:design-space-S}), one could imagine multiple levels of sophistication:
\begin{itemize}
  \item \textbf{Feature counts/capability profiles.} Treat $E$ as a monotone function of which macro-expressive facilities are present; treat $V$ as a monotone function of which classes of certificates are checkable under the intended discipline.
  \item \textbf{Human-facing measures.} Collaborate with HCI researchers to operationalize comprehensibility/interaction cost using established frameworks (e.g.\ cognitive dimensions) rather than anecdotes \cite{GreenPetre1996CogDims}.
  \item \textbf{Cost/complexity measures.} Refine the notion of ``verification/evaluation cost'' using machine-independent complexity measures in the sense of Blum-style axiomatizations, allowing comparisons that do not depend on a particular machine model \cite{Blum1967ComplexityAxioms}.
\end{itemize}
We treat such measurement programs as important but orthogonal: the EVT thesis concerns the existence and character of the boundary, not a definitive cartography of all languages.

\subsection{Attack Vectors Against the EVT}
\label{sec:attack-vectors}

One might ask whether a clever adversary could ``route around'' the EVT guardrails by hiding expressiveness or proof burden behind indirection. The short answer is: they can \emph{move} the difficulty around, but they cannot remove it.  In practice, such attempts tend to collapse into one of the three failure states: loss of correctness, loss of compilability, or loss of comprehensibility.

\medskip

\paragraph{Threat model.} Imagine an adversary with excellent taste in type theory. Their goal is to build a language that \emph{appears} to be simultaneously highly expressive, highly verifiable, and still friendly to humans and compilers (the three C's). What tricks might they try?

```latex
% Optional helper macro for compact attack-vector formatting.
% Place near the section, or in the preamble if reused.
\newcommand{\AttackVector}[4]{%
\item \textbf{#1}
\begin{description}[leftmargin=2.8em, style=nextline]
  \item[Attack.] #2
  \item[EVT response.] #3
  \item[Heuristic detector.] #4
\end{description}
}

\begin{enumerate}[leftmargin=2.2em]
  \AttackVector
    {Meta-languages and language embedding.}
    {Keep a tiny surface syntax that looks harmless, while embedding a full proof language inside the meta-level through macros, reflection, staging, or quotation.}
    {The proof/certificate workload still exists; it merely shifts phases. Either the compiler must normalize or check large meta-generated artifacts, producing loss of \emph{compilability}, or the user must reason about the meta-language to debug failures, producing loss of \emph{comprehensibility}.}
    {Elaboration or certificate-derivation size grows rapidly even when surface programs remain small.}

  \AttackVector
    {Type-level computation disguised as ``just types.''}
    {Allow type-level recursion, type families, implicit search, or dependent evaluation so that the type layer computes like the value layer, hiding substantial computation inside apparently simple signatures.}
    {Either the checker becomes unpredictable, producing loss of \emph{compilability}; the system imposes strict stratification or termination conditions, reducing $E$; or it risks G\"odel-style unsoundness, producing loss of \emph{correctness}.}
    {Type-dependency graphs and checking derivations exhibit high entanglement or width; local reasoning breaks down.}

  \AttackVector
    {``Semantics without syntax'': magical inference.}
    {Remove annotations and ask the compiler to infer nearly everything---types, proofs, equalities, coercions---so that the user writes pleasant code while the toolchain silently performs deep theorem proving.}
    {This is \Cref{sec:tarski-compiler} in disguise. Either inference/search diverges or blows up, producing loss of \emph{compilability}, or it becomes so opaque that fixing errors requires global expertise, producing loss of \emph{comprehensibility}.}
    {Long inference chains and non-local error explanations correlate with large derivations and wide dependency structure, although opacity is not fully captured by the present metrics.}
\end{enumerate}

\paragraph{Optional future metric: locality of repair.}
One plausible refinement---if adversaries get too clever---is to formalize a notion of \emph{annotation transparency} or \emph{locality of repair}:
\begin{quote}
A design is \emph{$k$-local} if, whenever type inference fails on a program $P$, there exists a correction that can be derived (or diagnosed) using only $O(k)$ lines of local context.
\end{quote}
We do not treat this as a new EVT axis here: it is difficult to formalize cleanly, and may be partially emergent from the structural-width proxies already discussed. But empirically, inference opacity is a primary failure mode in advanced typed systems: users do not quit because the system is unsound; they quit because they cannot \emph{repair} it.

\medskip
\noindent
\textit{Takeaway.} ``Cheating'' strategies mostly change \emph{where} the cost appears: in the compiler, in the proof artifacts, or in the user's head. The EVT is precisely the claim that, beyond a certain expressive/verifiable regime, we cannot avoid paying it somewhere.