\section{EVT: Scenarios and Failures} \label{sec:evt-failures} We now turn to the second half of the EVT: not the definitions of the axes, but the ways systems of computation begin to fail when pushed toward the boundary. Our strategy is to study \emph{failure modes} obtained by holding two constraints fixed (or ``high'') while attempting to maximize the remaining dimensions. Throughout this section, keep in mind the intended meaning of our guardrails: \begin{itemize} \item \textbf{Consistency.} Accepted proofs/certificates correspond to true semantic claims. \item \textbf{Compilability.} The elaboration--checking--evaluation pipeline has controlled (e.g.\ polynomial) overhead, as in \cref{sec:tractability}. \item \textbf{Comprehensibility.} The system remains usable as a human interface, rather than an opaque proof-search engine. \end{itemize} We treat comprehensibility as a distinct (human-facing) constraint even though it partially overlaps with our broader tractability discussion. \subsection{Gödel's Type System} \label{sec:godel-type-system} \textbf{Loss of Consistency.} A \emph{Gödel type system} (in our sense) is a type system in which \emph{the proof language is computationally universal} in a way that meaningfully interacts with typing/definitional equality. The name is meant to evoke Gödelian diagonalization: once sufficiently strong self-reference and computation are internalized, some combination of decidability, completeness, and consistency must fail. \begin{defn}[Gödel Type System] \label{def:godel-type-system} Let $\mathcal{T}$ be a type system with a distinguished empty/false type $\bot$ (``False'') and the Curry--Howard reading (types as propositions, terms as proofs) \cite{Howard1980FormulaeAsTypes}. We call $\mathcal{T}$ a \emph{Gödel type system} if there is a computable map \[ \langle M,x\rangle \longmapsto \tau_{M,x} \] from Turing machines $M$ and inputs $x$ to \emph{closed} types $\tau_{M,x}$ such that \[ \tau_{M,x}\ \text{is inhabited in }\mathcal{T} \quad\Longleftrightarrow\quad M\ \text{halts on input }x. \] Equivalently, the inhabitation problem for $\mathcal{T}$ is at least as hard as the halting problem. \end{defn} Even relatively disciplined polymorphic calculi already exhibit undecidable \emph{typability}/\emph{type-checking} problems in Curry-style formulations \cite{Wells1999SystemFUndecidable, Wells1994LICSUndecidable}. Gödel type systems are the ``maximal'' version of this phenomenon: once inhabitation can encode halting, no sound and complete mechanical verifier for inhabitation can exist. This failure mode occurs when one maximizes comprehensibility and compilability while still keeping a high level of expressiveness ($E$). This triggers an \emph{unsound} failure mode. \medskip This is the realm of a language where one can express quickly, compile fast, and understand easily. Only to be met with the situation where they must then remark \begin{center} \begin{quotation} \emph{``...hold a second, why did my proof of $1 = 0$ pass typechecking?''} \end{quotation} \end{center} \noindent The danger zone is precisely where the language is simultaneously expressive enough that nontrivial computation can be encoded \emph{at the proof/type level}, and engineered for fast, predictable checking, with a simple mental model. Under these pressures, systems frequently ``solve'' the conflict by silently weakening the meaning of ``proof accepted''---i.e.\ by becoming unsound. \paragraph{Core mechanism of failure.} At a high level, the pipeline is: \[ \text{(high $E$ at the type level)}\ \Longrightarrow\ \text{(general computation inside proofs)}\ \Longrightarrow\ \text{(loss of normalization/decidability)}. \] At that point, there are only a few options: \begin{enumerate}[label=(U\arabic*), leftmargin=3.2em] \item sacrifice tractability (permit expensive/global proof search or heavy automation), \item sacrifice expressiveness (restrict recursion/effects; stratify universes), \item or sacrifice soundness (accept an incomplete/approximate kernel that may accept bogus inhabitants of $\bot$). \end{enumerate} The unsound failure mode is (U3). A canonical way soundness collapses is by admitting \emph{general recursion as proof}. \begin{prop}[General recursion trivializes the logic] \label{prop:general-recursion-trivializes} Let $\mathcal{T}$ be a Curry--Howard style type system with: \begin{enumerate}[label=(H\arabic*), leftmargin=3.2em] \item an empty type $\bot$ and an elimination principle $\mathsf{exfalso}_A : \bot \to A$ for every type $A$ (principle of explosion), and \item a fixed-point operator $\mathsf{fix}_A : (A\to A)\to A$ for every type $A$ (general recursion at the term/proof level). \end{enumerate} Then every type $A$ is inhabited (the logic is inconsistent). \end{prop} \begin{proof} Let $f \triangleq (\lambda x{:}\bot.\ x) : \bot \to \bot$. Define \[ \mathsf{loop} \triangleq \mathsf{fix}_{\bot}(f) : \bot. \] Then for any $A$, define $\mathsf{explode}_A \triangleq \mathsf{exfalso}_A(\mathsf{loop}) : A$. \end{proof} \textbf{Coq vs. Idris on type safety.} Proof assistants based on normalization (e.g.\ Coq's CIC) enforce termination/guardedness conditions precisely to prevent \cref{prop:general-recursion-trivializes}. Coq's kernel uses a syntactic guardedness/structural recursion criterion (the ``guard condition'') rather than admitting unrestricted fixed points \cite{Gimenez1995GuardedDefs, Barras2006GuardCondition, CoquandHuet1988CoC}. But what if we allow general recursion at the proof level? Imagine we write something like this in a dependently typed language \emph{without} a termination/totality discipline enforced by the kernel (or with it disabled) \cite{Brady2013Idris}: \begin{verbatim} loop : False loop = loop \end{verbatim} \noindent This defines a ``proof'' of \texttt{False} that is just itself. Once we have \texttt{loop : False}, we can write: \begin{verbatim} explode : a explode = case loop of {} \end{verbatim} \noindent This is the principle of explosion: from $\bot$ one can produce anything. In other words, once $\bot$ is inhabited, \emph{every} proposition becomes provable, and the proof system collapses. \paragraph{Formal version: the Curry paradox.} The above is one route (general recursion). A second, more ``Gödelian'' route is \emph{self-reference}. Curry's paradox shows that if a system admits sufficiently strong self-referential propositions of the form \[ C \;\leftrightarrow\; (C \to F), \] then it can derive the arbitrary conclusion $F$ (hence prove everything) \cite{Curry1942Inconsistency,Shapiro2017CurryParadoxSEP}. One clean way to package this for the EVT is as a schema. \begin{prop}[Curry fixed-point schema implies triviality] \label{prop:curry-schema} Work in a logic/type theory with implication and contraction. Assume the following \emph{fixed-point schema}: for every formula/type-valued expression $\varphi(X)$ (with $X$ occurring only positively), there exists a closed formula/type $C$ such that \[ C \;\leftrightarrow\; \varphi(C). \] Then for every formula $F$, the logic proves $F$. \end{prop} \begin{proof}[Proof sketch] Take $\varphi(X)\triangleq (X\to F)$, so $C \leftrightarrow (C\to F)$. From $C$ and $C\to F$, we get $F$ by modus ponens. But $C$ also implies $C\to F$, so one can derive $C$ and hence $F$; Curry's original presentations isolate exactly which structural rules are responsible (notably contraction). \end{proof} \paragraph{Type-theoretic analogues.} Type theories encounter Curry-like self-reference pressures whenever they blur critical stratifications: e.g., \ collapsing universe levels (``Type : Type'') yields Girard/Hurkens-style paradoxes that derive $\bot$ \cite{Coquand1986GirardParadox, Hurkens1995GirardSimplification}. Modern proof assistants, therefore, pay an explicit complexity tax (universe hierarchies, guarded recursion, syntactic restrictions) to remain sound. This failure mode is the cautionary tale behind the First Law. If one wants: \begin{itemize} \item a language that is easy to write and understand (high comprehension), \item a compiler/checker that runs fast and predictably (high compilability), \item and also type-level expressiveness that can internalize serious computation (high $E$), \end{itemize} then they are constantly tempted toward Gödelian constructions: either general recursion sneaks into proofs, or self-reference/impredicativity collapses the stratification that keeps the logic consistent. Unless one imposes strong guardrails (totality/termination, universe stratification, restricted reflection), the system becomes unsound. \medskip \noindent\textit{In summary.} The type system eats the language. \subsection{Tarski's Compiler} \label{sec:tarski-compiler} \textbf{Loss of Compilability.} A \emph{Tarski compiler} is a compiler (more broadly: an elaborator/typechecker pipeline) that is asked to produce \emph{truth inside itself}. \medskip The name is deliberate. Tarski’s undefinability phenomenon can be summarized informally as: once a system is expressive enough to encode arithmetic, it cannot contain a truth predicate for its own sentences satisfying the full ``$T$-schema'' without collapse \cite{Tarski1936Truth}. We use this as an analogy---not a literal reduction---for what happens when a language design tries to make the compiler silently discharge arbitrary semantic obligations while remaining both correct and human-friendly. \paragraph{Compilability as a working constraint.} In the scenario analysis, \emph{compilability} is the requirement that the compilation pipeline is a \emph{total, predictable procedure}: given a program, it should either (a) produce compiled output, or (b) reject with a diagnostic, within controlled resource bounds. When compilation includes elaboration, implicit argument inference, unification, and proof search, compilability becomes a substantive constraint rather than a default expectation. \begin{defn}[Tarski compiler] \label{def:tarski-compiler} Fix a language $L$ whose static discipline expresses a class of propositions/specifications $\Phi$ (often via types). A compiler pipeline $\mathsf{Comp}$ for $L$ is called a \emph{Tarski compiler} if it is expected to satisfy all three of the following: \begin{enumerate}[label=(TC\arabic*), leftmargin=3.2em] \item \textbf{Consistency.} Whenever $\mathsf{Comp}$ accepts a program, the accepted implicit obligations are semantically valid (soundness of compilation and checking). \item \textbf{Comprehensibility.} Programmers may omit large parts of the proof/annotation burden; the system attempts to infer or synthesize missing logical structure ``in the background.'' \item \textbf{Internal truth production.} For a wide class of implicit obligations $\varphi \in \Phi$, the compiler is expected to \emph{decide} (or effectively settle) whether $\varphi$ holds, as part of determining whether the program compiles. \end{enumerate} \end{defn} The tension is immediate: (TC3) is a demand that compilation act like a truth oracle for a rich internal logic, while (TC2) shifts responsibility from the human to the compiler. This is the second failure state, the \emph{Tarski Compiler}. It occurs when one designs a language that is highly expressive ($E$) and insists on consistency (soundness/verifiability), but also tries to remain comprehensible---meaning that ordinary programmers can write code without supplying full formal proofs. The goal is to remain powerful and safe, but still human-friendly; then the price is that the compiler inherits the missing work: elaboration becomes proof search. \paragraph{Core mechanism of failure.} The design typically includes all of the following: \begin{itemize} \item a static logic expressive enough to encode nontrivial propositions (e.g.\ dependent types, rich refinement constraints, higher-order encodings); \item a correctness mandate: accepted programs must come with valid certificates (explicit or implicit); \item an ergonomic mandate: the user does not write the certificates in full, so the compiler tries to infer/synthesize them. \end{itemize} \noindent As a result, compilation begins to include: \begin{itemize} \item \textbf{Typechecking as theorem proving.} ``Does this elaborate/typecheck?'' becomes ``is there a proof of this obligation?'' \item \textbf{Inference as proof search.} The compiler runs search procedures (unification, instance resolution, tactic-like automation). \item \textbf{Compile-time nontermination/blowup.} These procedures are, in general, not guaranteed to terminate or to remain within predictable bounds. \end{itemize} The issue is that the compiler is forced into semi-decision procedures. The moment the compiler is responsible for \emph{finding} proofs rather than merely \emph{checking} them, it inherits the meta-theoretic limits of proof search. Even when the kernel checking problem is decidable (as it often is in normalization-based systems), the \emph{synthesis} and \emph{inference} problems that make the system comprehensible can be undecidable or only semi-decidable. A canonical example is \emph{higher-order unification}, which arises naturally during elaboration of dependently typed terms; it is not decidable in general and is typically handled by search/backtracking heuristics \cite{Huet1975Unification, Huet1976Unification}. \begin{prop} \label{prop:infinite-compiler-structural} Assume a language $L$ whose specification logic $\Phi$ is expressive enough that proof existence (inhabitation) can encode an undecidable problem (e.g.\ the halting problem, as in \cref{def:godel-type-system}). Consider a compiler pipeline that aims to satisfy: \begin{enumerate}[label=(\alph*), leftmargin=2.8em] \item correctness (soundness: it never accepts false obligations), and \item comprehensibility (it attempts to infer/synthesize omitted proof obligations from a broad class). \end{enumerate} Then, in general, the pipeline cannot satisfy compilability as a total decision procedure (always halts with accept/reject) for that broad class of programs/obligations. \end{prop} \begin{proof}[Proof sketch] If the compiler always halts and is correct, and if it is also sufficiently complete about inferring the omitted obligations (so that ``easy to write'' programs are accepted whenever the corresponding obligations are true), then it would decide truth/existence of proofs for a class of obligations that can encode an undecidable problem. This contradicts the assumed expressiveness of $\Phi$. Therefore, at least one of the desiderata must fail: either the compiler becomes incomplete (rejects/gets stuck on true programs), or it becomes nonterminating/unpredictable (loss of compilability), or the soundness/correctness guarantee is weakened. \end{proof} \paragraph{Real-world examples.} This failure mode is the compiler being asked to do the following, on demand: \begin{quote} \textit{``Here is a vague, high-level, partially specified statement. Please reconstruct the missing formal proof that makes it valid, and do so while I wait for compilation.''} \end{quote} \noindent Sometimes the proof does not exist. Sometimes it exists but requires a search space so large that compilation becomes effectively unbounded. In the limit, compilation becomes an interactive theorem-proving session that has been hidden behind the \texttt{build} command. This phenomenon is visible whenever automation is made ``too helpful'' in expressive proof-oriented languages: \begin{itemize} \item In Coq, aggressive automation and search (e.g.\ \texttt{auto}, \texttt{eauto}, typeclass resolution) can lead to severe performance degradation or nontermination on poorly constrained goals; practitioners mitigate this with search bounds, hints databases discipline, and explicit proof structure.\footnote{This is not a criticism of Coq: it is an illustration that \emph{proof search} is a different computational regime than \emph{proof checking}.} \item In Agda (and related systems), elaboration and instance search similarly require careful scoping and user guidance to avoid runaway search. \end{itemize} \medskip \noindent\textit{In summary.} The language eats the compiler. \subsection{Rice's Revenge} \label{sec:rice-revenge} \textbf{Loss of Comprehensibility.} \emph{Rice's Revenge} occurs when a language's sophistication exceeds its user base. \medskip A natural objection to the EVT is: if a type system is powerful enough, why can we not have maximal expressiveness and maximal verifiability simultaneously? Wouldn't paradoxes (Gödel-style) or nontermination (Tarski-style) automatically prevent a system from becoming ``too perfect''? Why introduce a third, seemingly opaque axis about human brains? The missing point is that ``verification'' is not a free property one adds on top of a language. It is itself a \emph{language of certificates}---typing derivations, coercions, proof terms, solver traces, or tactic scripts---together with a kernel that checks them. Once a system is sufficiently expressive, the certificate language becomes a programming language in its own right, with its own search problems, its own size blowups, and its own usability constraints. In other words: \[ \text{(rich specs)} \quad \Rightarrow \quad \text{(rich proof objects)} \quad \Rightarrow \quad \text{(somebody must build them)}. \] If the compiler builds them, we risk the \emph{Tarski Compiler} (loss of compilability). If the compiler accepts them without adequate checking, we risk \emph{Gödel's Type System} (loss of correctness). The remaining option is that the \emph{programmer} builds them---and that is where comprehensibility becomes a hard constraint rather than a cosmetic one. This is the third failure state. It arises when we insist on: \begin{itemize} \item \textbf{Consistency.} Accepted programs really satisfy their specifications (soundness), and \item \textbf{Compilability.} Compilation/checking remains a predictable, terminating procedure, \end{itemize} while also pushing expressiveness $E$ and verifiability $V$ very high. The only remaining place for the irreducible difficulty to go is the \emph{user}. \paragraph{A minimal formal model: explicit certificates.} Fix a surface language $L_{\mathsf{surf}}$ and an explicitly typed/certified core $L_{\mathsf{core}}$. Think of $L_{\mathsf{core}}$ as the language in which all implicit proof obligations have become explicit terms (coercions, proof arguments, equality witnesses, termination metrics, etc.) This ``explicit core'' pattern is standard in the design of verified compilers and proof-oriented languages: it is how one keeps the kernel small and checking syntax-directed. \begin{defn}[Proof-carrying elaboration interface] \label{def:proof-carrying-elab-interface} A proof-carrying compilation interface consists of: \begin{enumerate}[label=(PC\arabic*), leftmargin=3.2em] \item a checkable judgment in the core (typechecking/certificate checking) \[ \vdash_{\mathsf{core}} Q : \tau \] that is decidable (or at least engineered to be reliably terminating) for $Q\in L_{\mathsf{core}}$; \item an erasure/forgetful map $\mathsf{erase}: L_{\mathsf{core}}\to L_{\mathsf{surf}}$; \item an elaboration relation producing \emph{some} certificate-bearing core term for a given surface term: \[ P \leadsto Q \quad\text{with}\quad \mathsf{erase}(Q)=P. \] \end{enumerate} \end{defn} This interface makes a clean separation: \begin{itemize} \item \emph{checking} is tractable/decidable (compilability preserved), and \item \emph{finding} the missing certificates is an additional problem not guaranteed to be automatic. \end{itemize} (See, e.g., the explicit-core approach in dependent extensions of Haskell, where decidable, syntax-directed checking is recovered by carrying explicit equality/coercion evidence \cite{WeirichEtAl2017DependentHaskell}.) \paragraph{Rice's theorem pressure: why inference cannot save us in general.} Rice's theorem says that every nontrivial extensional semantic property of programs is undecidable. While Rice is classically stated for partial computable functions, the moral transfers directly: once a specification language is rich enough to express nontrivial behavioral claims, there is no general total procedure that can infer (or decide) those claims from arbitrary programs. This yields the ``revenge'': \begin{quote} \textit{If one wants consistency and compilability in a highly expressive verification regime, then one cannot hide the semantic difficulty in the compiler. The difficulty reappears as proof burden and annotation burden for the human.} \end{quote} \begin{prop}\label{prop:comprehensibility-hard-constraint} Assume a setting where the verified meaning of a program requires producing certificate artifacts (proofs, coercions, termination evidence, etc.) that are checked by a sound, terminating kernel. If the property class being enforced includes nontrivial semantic properties (in the sense of Rice), then there is no general algorithm that, for all programs, can automatically synthesize the required certificates while remaining both correct and terminating. Therefore, preserving consistency and compilability forces certificate construction to become (at least partially) an interactive, user-driven activity---which can destroy comprehensibility at scale. \end{prop} \begin{proof}[Proof sketch] If a compiler were to (a) always terminate, (b) be correct (sound), and (c) automatically synthesize certificates for a sufficiently rich class of semantic obligations, then it would decide a nontrivial semantic property class uniformly, contradicting Rice-style undecidability. Hence, at least one of (a)--(c) must be relaxed. In this failure state, we refuse to relax (a) and (b), so we necessarily relax (c) by shifting work to the programmer. \end{proof} \paragraph{The core mechanism of the failure.} In a system that remains correct and compiler-friendly, the ``missing work'' manifests as explicit proof structure: termination arguments, invariants, equality rewrites, and transports. Even when each individual proof step is local, the aggregate burden can be overwhelming. The result is a system that is sound and predictable but only usable by a small population trained to manage proof objects and their algebra. \medskip To illustrate the third failure state, let us consider the construction of a hypothetically \emph{maximally verifiable} and \emph{maximally expressive} programming language. Introducing \textsc{MAXlang}\texttrademark. \medskip \paragraph{Design slogan.} \textsc{MAXlang} aims to be: \begin{itemize} \item \textbf{Maximally expressive.} Full general recursion, effects, metaprogramming, reflection, the works. \item \textbf{Maximally verifiable.} Every exported behavior must come with a machine-checkable certificate. \item \textbf{Compiler-friendly.} The kernel only \emph{checks} certificates; it does not perform open-ended proof search. \end{itemize} In other words, \textsc{MAXlang} preserves consistency and compilability by making the programmer supply whatever the logic requires. The result is predictable compilation---at the cost of comprehensibility. \medskip \paragraph{A small program in \textsc{MAXlang}.} Here is ``hello world''---not in the sense of printing a string, but in the sense of performing a mundane task: sorting a list of integers. \begin{quote}\small \begin{verbatim} module Demo.Sort -- Built-ins (informal): Nat, Int, List, (<=), etc. -- Dependent subset type {x : A | P x} is written: Subset A P -- Proof terms are explicit; rewriting requires explicit equality transport. -- Termination is required for definitional equality; general recursion exists -- but must carry an explicit semantic certificate when exported. -- A predicate that a list is sorted. Sorted : List Int -> Type Sorted [] = Unit Sorted [x] = Unit Sorted (x :: y :: t) = (x <= y) × Sorted (y :: t) -- A predicate that two lists are permutations (multiset equality). Perm : List Int -> List Int -> Type Perm xs ys = (CountEq xs ys) -- assume standard multiset counting spec -- The "specification type" for a sorting function: -- It must return a list that is sorted AND is a permutation of the input. SortSpec : Type SortSpec = (xs : List Int) -> { ys : List Int | Sorted ys × Perm xs ys } -- Now we write insertion sort, but MAXlang requires evidence at each step. insert : (x : Int) -> (ys : List Int) -> { zs : List Int | Sorted ys -> Sorted zs × Perm (x :: ys) zs } insert x [] = [x] with proof Sorted[]ToSorted[x] : Sorted [] -> Sorted [x] proof PermInsertNil : Perm (x :: []) [x] insert x (y :: t) = if x <= y then (x :: y :: t) with proof SortedInsertFront : Sorted (y :: t) -> Sorted (x :: y :: t) proof PermInsertFront : Perm (x :: (y :: t)) (x :: y :: t) else let rec = insert x t in let zs = rec.value in (y :: zs) with proof SortedInsertTail : (Sorted (y :: t)) -> (Sorted zs) -> (y <= head zs) -> Sorted (y :: zs) proof PermInsertTail : Perm (x :: (y :: t)) (y :: zs) -- The actual sort function. sort : SortSpec sort [] = [] with proof TrivialSortedNil : Sorted [] proof TrivialPermNil : Perm [] [] sort (x :: t) = let ih = sort t in let ys = ih.value in let prS = ih.proof.left in -- Sorted ys let prP = ih.proof.right in -- Perm t ys let ins = insert x ys in ins.value with proof FinalSorted : -- combines prS with the insert proof: Sorted (ins.value) proof FinalPerm : -- combines prP with the insert proof: Perm (x :: t) (ins.value) \end{verbatim} \end{quote} There is nothing exotic about sorting. The burdensome part is that \textsc{MAXlang} forces every mundane function to carry: \begin{itemize} \item a \emph{semantic specification} (here: sortedness and permutations), \item explicit proof terms (or proof skeletons) for every nontrivial step, \item explicit transports/rewrites (hidden above behind the word \texttt{proof}). \end{itemize} The kernel remains small, and compilation remains predictable---because the compiler is not searching for these proofs. But the \emph{surface language} has become a proof engineering environment, even for tasks that normal programmers expect to be one screen of code. \medskip \noindent\textit{In summary.} The language eats the programmer. \begin{table}[htbp] \centering \caption{Failure Modes of the EVT Trilemma} \label{tab:sl_failure_modes} \renewcommand{\arraystretch}{1.5} % Adds a bit of breathing room between rows \begin{tabular}{@{} p{3cm} p{3.5cm} p{5.5cm} l @{}} \toprule \textbf{Preserved} & \textbf{Broken Constraint} & \textbf{Resulting Pathology} & \textbf{Failure Mode} \\ \midrule Consistency \newline Compilability & Comprehensibility & Programmers need to be PhDs in Category Theory and Modal Logic to use the language & Rice's Revenge \\ Consistency \newline Comprehensibility & Compilability & A compiler or interpreter may never halt due to undecidable analyses or infinite proof search & Tarski Compiler \\ Compilability \newline Comprehensibility & Consistency & Language is pleasant to use, but makes no guarantees about behavior or correctness & Godel Type System \\ \bottomrule \end{tabular} \end{table} \medskip Hence, for any sufficiently expressive language, there exists a bound on the combined achievable levels of expressiveness, verifiability, and comprehensibility. Pushing all three to their extremes leads to logical inconsistency (breakdown of soundness), algorithmic intractability (undecidability or non-termination of analysis), or human incomprehensibility (cognitive overload). \subsection{Landin's Ghost?} \label{sec:landins-ghost} \textbf{On hardware intolerance and expressivity.} Even if it could be designed, \textsc{MAXlang} will likely never run on commodity hardware in the way ordinary ``general-purpose'' languages do. Why might this be the case? \medskip Landin’s remark about delivering \textsc{Lisp} from ``hand-to-mouth storage allocation'' is a clue: the expressive affordances of a language are never purely syntactic. They come with a runtime model (allocation, representation, control, effects), and that runtime model has a \emph{hardware footprint}. Historically, when the footprint was large enough, it motivated building machines around the language. \paragraph{Hardware intolerance.} We will call a language \emph{hardware-tolerant} if it admits efficient implementations on a stable, commodity execution substrate (a fixed ISA and memory hierarchy), without requiring language-specific microarchitectural support beyond what is already ubiquitous. Conversely, a language is \emph{hardware-intolerant} when its dominant costs are tied to semantic mechanisms that are poorly matched to the commodity substrate, so that acceptable performance requires either (a) extensive dynamic compilation machinery, or (b) specialized hardware support. This is not meant as a sharp complexity-theoretic classification; it is an engineering distinction. Its purpose in the EVT is to explain why ``maximal'' expressiveness tends to drag the execution platform along with it. \paragraph{Why the Lisp Machine existed.} The MIT Lisp Machine project is the canonical example of hardware intolerance being treated as a first-class design constraint. The goal was not merely to run \textsc{Lisp} \emph{at all}, but to run it efficiently by moving key semantic mechanisms into the architecture: tagged representations (data with built-in type fields), microcoded support for high-level operations, and storage-management features such as garbage collection tightly integrated with the machine model \cite{Bawden1977LispMachineProgress, Greenblatt1980LispMachine, Moon1984GCLargeLispSystem}. The design philosophy is explicit in the literature: Lisp machines are ``high-level language computer architectures,'' where the boundary between ``language runtime'' and ``hardware'' is intentionally blurred \cite{Steele2002EvolutionOfLisp, Weinreb1981LispMachineManual}. On that reading, Landin’s warning is not aesthetic. It is architectural: certain forms of expressivity (especially those built around pervasive allocation, dynamic representation, and reflective control) create a pressure gradient toward bespoke execution support. \paragraph{Modern day situation.} But excluding computer history museums, retro-hacker conventions, or perhaps the basements of various DARPA/Air Force research labs, one does not find working Lisp machines.\footnote{The rumor that Symbolics Lisp Machines were the main backbone behind the infamous Cold War era ``Star Wars'' program was, in all likelihood, an elaborate hoax perpetrated by early Usenet trolls.} Modern commodity computing largely converged on a small number of ISA families and broadly ``RISC-like'' microarchitectural principles, driven by VLSI design constraints, toolchain/ecosystem lock-in, and economies of scale \cite{PattersonDitzel1980RISC}. Even when contemporary CPUs are not purely RISC in an ISA sense, their performance envelope is dominated by a standardized substrate: pipelines, caches, branch predictors, SIMD, and a memory hierarchy optimized for common workloads. In such an environment, languages that demand unusual runtime services must either simulate them in software (VMs, JITs, GC) or accept large constant factors. \paragraph{Kogge and the architecture of symbolic computers.} A complementary perspective comes from Peter Kogge’s textbook \emph{The Architecture of Symbolic Computers}, which treats ``symbolic'' execution models (functional and logic language computing, dynamic representations, heap-centric computation, graph reduction, pattern-driven control) as architectural first-class citizens rather than mere software conventions \cite{Kogge1991SymbolicComputers}. Kogge’s central theme aligns with the Lisp Machine lesson: once a language’s semantic core relies heavily on mechanisms such as tagged representations, pervasive allocation, indirect addressing, and runtime-managed structure (including garbage collection), the performance-critical path is no longer ``a fast inner loop'' on a stable instruction set, but a tight interplay between evaluation strategy, memory system behavior, and runtime services. In such regimes, the naive von Neumann/RISC abstraction (a fixed ISA executing a uniform stream of instructions over unstructured memory) becomes a poor semantic match. Efficiency pressures naturally reintroduce language-specific support: either in the architecture (tags, specialized primitives, microcode-like support) or in an increasingly elaborate compilation/runtime tower (JITs, staged specialization, and aggressive representation management). This is precisely the sense in which highly expressive symbolic substrates can become \emph{hardware-intolerant}: the more the language shifts computation into rich runtime structure, the more the ``machine'' must effectively internalize that structure to execute it efficiently. \paragraph{\textsc{MAXlang} pushes the pressure to the limit.} \textsc{MAXlang} is intentionally designed to maximize expressiveness and verifiability. But note what that means operationally: \begin{itemize} \item \emph{Expressiveness} pushes semantic phenomena into the language (reflection, metaprogramming, rich effects, intensional equality, etc.). \item \emph{Verifiability} pushes obligations into the static world (proof terms, equality witnesses, termination/totality artifacts, refinement evidence). \end{itemize} The combined result is that a ``program'' is no longer merely an instruction stream. It is a coupled object: code \emph{plus} certificates \emph{plus} a meta-level that may compute with those certificates. At that point, the classical separation between ``compile'' and ``run'' becomes unstable. One principled way to see this is through program specialization: compilation can be viewed as specializing an interpreter (or semantic evaluator) to a fixed source program (Futamura’s perspective) \cite{Futamura1999PartialEvalCompilerCompiler, JonesGomardSestoft1993PEBook}. When the semantic apparatus is simple, specialization yields a stable target (machine code for a fixed ISA). When the semantic apparatus includes rich metalevel computation and proof-relevant evaluation, efficient execution increasingly looks like \emph{specializing the evaluator itself} to the particular program’s proof obligations and reflective behavior. In the limit, \emph{each program induces its own optimal abstract machine}. This is the precise sense in which ``every program defines its own hardware'': not that literal silicon must be fabricated per program, but that a fixed universal substrate becomes a poor match. The natural endpoint is either: \begin{itemize} \item a tower of staging/JIT/specialization machinery that effectively synthesizes a program-specific execution strategy, or \item reconfigurable computing (microcode/FPGA-like specialization), where the ``instruction set'' is itself a residual artifact of compilation. \end{itemize} Either way, the notion of a single, uniform ``universal processor'' that runs \textsc{MAXlang} efficiently for all programs becomes aspirational rather than realistic. Taken together, they explain why a universal ``do-what-I-mean'' compiler cannot exist: a compiler that is asked to be both reflective and semantically omniscient is being asked for a truth predicate over its own behavioral universe. On the physical side, there are genuine thermodynamic limits on information processing (e.g.\ Landauer’s principle relating logical irreversibility to heat dissipation) \cite{Landauer1961Irreversibility}. We invoke such results only as a reminder that computation is not free: unbounded elaboration, unbounded proof normalization, and unbounded meta-level execution are not merely theoretical inconveniences---they collide with finite time, energy, and memory. \paragraph{Landin’s warning, updated.} Landin’s gumblings about Lisp’s appetites (allocation discipline, pedagogical heaviness, syntactic and semantic overhead) read today like a warning about the whole ``maximal language'' fantasy \cite{Landin1966Next700}. In the \textsc{MAXlang} limit, the appetite is no longer just for heap cells; it is for compilation effort, proof artifacts, and meta-level computation. And in an era of LLM-aided programming, where abstraction layers can be generated faster than they can be understood, the pressure toward hardware-intolerant semantics is stronger rather than weaker.