cs.LO — Logic in Computer Science
Expressiveness, Verifiability, Tractability: Toward a Computational Thermodynamics
An investigation into the existence of a conservation law governing computational behaviour, in the form of the Expressiveness, Verifiability, Tractability (EVT) Hypothesis, is undertaken. The hypothesis is motivated by a simple observation: mechanisms that increase what a system can directly express, powerful control, effects, reflection, meta-programming, and self-interpretation, tend to undermine what can be verified uniformly and mechanically, while regimes that maximize static guarantees typically do so by restricting expressiveness or relocating effort into compilers, proof artifacts, or human interpretation. We analyze canonical failure modes that arise when one attempts to push beyond this frontier, distinguishing collapse of correctness, collapse of compilability, and collapse of comprehensibility. We then develop an order-theoretic model for comparing languages and verification disciplines and define an “E/V boundary” as a Pareto frontier in a partially ordered design space. Finally, we sketch how analogous tradeoffs appear in other computational domains, suggesting that “thermodynamic” boundary behaviour may be a recurring feature of expressive formalisms that demand strong global guarantees and within physical methods of information processing.