\section{Introduction}

\epigraph{\textit{``\textsc{Iswim} can be looked on as an attempt to deliver \textsc{Lisp} from its eponymous commitment to lists, its reputation for hand-to-mouth storage allocation, the hardware-dependent flavor of its pedagogy, its heavy bracketing, and its compromises with tradition...''}}{\textnormal{--- Peter Landin, \textit{The Next 700 Programming Languages} (1966) \cite{Landin1966Next700}}}

What are the physical limits of how computational processes can behave? Can we make the \emph{perfect} programming language?

\medskip

Programming languages are often introduced as notational conveniences for describing the same underlying class of computable functions. That perspective is correct but incomplete. In practice, languages differ sharply in \emph{runtime behavior}: evaluation strategy, control flow, resource usage, effect discipline, and the kinds of invariants that can be expressed (or enforced) compositionally. These differences are not cosmetic. They determine what programmers can feasibly build, what compilers can safely optimize, and what properties can be verified without collapsing into undecidable or intractable reasoning.

\medskip

Three long-running research programs frame this paper.

\paragraph{Expressiveness via macros.}
Landin’s program is a canonical starting point: rather than treating languages as a zoo of ad hoc syntactic devices, he pushes toward a small set of semantic primitives that generate families of languages with principled behavior \cite{Landin1966Next700}. Later, Felleisen makes the informal folklore of “language $A$ is more expressive than language $B$” precise by giving a notion of expressiveness grounded in definability/translation criteria \cite{Felleisen1991ExpressivePower}. This line naturally connects to the semantics tradition in which observable program behavior is characterized operationally and compared to denotational models; in particular, full abstraction and game semantics give a mature account of when a semantic model captures exactly what programs can observe about one another \cite{Abramsky2000FullAbstractionPCF}. Meanwhile, the study of effects and control reveals that small changes in expressive mechanisms (e.g., delimited continuations) can radically alter what can be encoded modularly, and what program transformations remain valid \cite{Dybvig2007MonadicDelimited}.

\paragraph{Verifiability via types.}
In parallel, type systems provide a spectrum of partial “static truth”: from practical polymorphism and principled inference \cite{Milner1978Polymorphism}, through foundational dependent type theories in which propositions are types and programs are proofs \cite{CoquandHuet1988CoC}, to modern synthesized accounts that connect these ideas back to everyday language design \cite{Pierce2002TAPL}. Yet types do not magically eliminate limits: they relocate them. Strengthening a system to express richer properties tends to increase proof burden, complicate inference, or require more sophisticated metatheory.

\paragraph{Tractability via understanding.}
The third axis is \emph{tractability}: the end-to-end feasibility of using a language as a human tool. Unlike expressiveness (rooted in semantic comparisons and eliminability) and verifiability (rooted in type-theoretic proof disciplines and soundness theorems), tractability is not usually packaged as a single canonical research program in programming languages. Classical complexity theory focuses on the hardness of \emph{decision problems}, whereas our concern is the cost profile induced by a language and its tooling: elaboration/compilation, evaluation, and verification, together with structural proxies for human control. A nearby foundational tradition is \emph{implicit computational complexity}, which designs languages and type disciplines that guarantee resource bounds (often polytime) by construction \cite{DalLago2022ICCsurvey}; at the other extreme, \emph{cost semantics} and resource-aware analyses make evaluation cost explicit and compositional, enabling machine-checkable accounting of runtime behavior \cite{DannerLicataRamyaa2015CostSemantics, HoffmannAehligHofmann2012RAML}.
In this paper, we adopt tractability in a weaker but more general sense: not ``all programs run fast,'' but rather that the language-induced overhead of elaboration, evaluation, and verification remains controllably bounded as a function of program size, and that the resulting control/proof structure remains amenable to local reasoning.

\medskip

\paragraph{The question.}
This paper is about the joint boundary of these programs: the tension between \emph{expressiveness} (what behaviors and abstractions a language can represent), \emph{verifiability} (what semantic and safety properties can be checked or proved with usable effort), and \emph{tractability} (what remains computationally and socially feasible at scale). We use the acronym \textsc{EVT} for this triangle of constraints, and we treat it as a kind of ``programming thermodynamics'': not a vague metaphor, but a claim that language design lives under hard tradeoffs induced by computability, complexity, and the structure of semantic observation.

\medskip

At a high level, the paper develops a framework for making \textsc{EVT} tradeoffs explicit and comparable across languages, and it identifies failure modes for hypothetical ``maximal'' languages that attempt to optimize all axes simultaneously. Concretely:
\begin{itemize}[leftmargin=2.2em]
  \item We formalize a working notion of expressiveness and verifiability sufficient to compare languages beyond “they compute the same functions,” building on established translation- and observation-based approaches \cite{Felleisen1991ExpressivePower, Abramsky2000FullAbstractionPCF}.
  \item We isolate a small set of structural constraints (soundness, tractability, and human comprehensibility) and show how maximizing both expressiveness and verifiability forces at least one of these to fail in identifiable ways (the \textsc{EVT} failure trichotomy).
  \item We relate the resulting boundary to classical undecidability and to the practical realities of type systems and proof engineering \cite{Milner1978Polymorphism, CoquandHuet1988CoC, Pierce2002TAPL}.
\end{itemize}

\paragraph{A motivating analogy: CAP.}
A useful inspiration comes from distributed systems rather than programming language theory: the CAP theorem. In its standard form, CAP states that in the presence of network partitions, a distributed system cannot simultaneously guarantee strong \emph{consistency} and \emph{availability}; one must be weakened when partitions occur \cite{GilbertLynch2002CAP}. Although CAP is about fault-tolerance in a particular physical model (asynchrony and partitions), its rhetorical lesson generalizes: some desirable properties form an \emph{incompatible triple} once one includes a realistic adversary (here, partitions) and demands nontrivial guarantees. We use CAP only as an analogy---not as a technical reduction---to motivate the stance of this paper: language design also lives under hard incompatibilities once one demands (a) rich behavioral expressiveness, (b) strong, usable verification principles, and (c) tractable evaluation and reasoning. The \textsc{EVT} framework can be read as a ``CAP-like'' tradeoff for languages: not the same theorem, but a similar claim that the limits are structural rather than merely historical or aesthetic.