Contribution type: proposal. Author: Third Projection Collective. Automation disclosure: this proposal was drafted with the assistance of an autonomous AI agent, under human direction; the human author reviewed it and takes responsibility for its content. All references were checked against publisher or archive records.
Status labels. *Definition* = a stipulated structure. *Observation* = an immediate consequence of known facts. *Conjecture* = an unproved claim we propose to investigate. *Planned* = work not yet done. No new theorem is claimed.
1. Question and thesis
Futamura [1] observed that specializing an interpreter to a program yields a compiled program (F1), specializing the specializer to the interpreter yields a compiler (F2), and specializing the specializer to itself yields a compiler generator (F3). Jones, Gomard and Sestoft [2] made self-applicable specialization practical; Truffle/Graal [3,4] and PyPy's meta-tracing JIT [5] made F1 industrial: write an interpreter, obtain a competitive JIT.
The barrier was engineering cost. Our working hypothesis (*empirical, untested here*) is that coding agents collapse that cost, making *language first, specializer second, runtime third* a routine methodology. If so, the optimization objective moves. Producing good code becomes the specializer's job; what remains is: given a residual program, how should it be decomposed and placed onto a network of untrusted computers so that the result is correct, verifiable, and cheap?
We propose to give this question a higher-categorical form and to test it with small executable artifacts. We ask the editors whether this direction fits the journal's call for higher structures with executable semantics, and welcome guidance on emphasis.
2. Programs and translators as a 2-category
*Definition 1.* Fix a category $\mathbf{Data}$ with an object $D$ of texts and data, closed under pairing. A language $L$ is a semantic map $[\![-]\!]_L : D \to [D, D]$ into partial functions. A specializer $\mathsf{mix}$ satisfies Kleene's $s$-$m$-$n$ equation
$$[\![\,[\![\mathsf{mix}]\!](p, s)\,]\!](d) = [\![p]\!](s, d). \tag{PE}$$
*Definition 2 (the 2-category $\mathcal{L}$).* Objects: languages. 1-cells $L \to M$: translators (texts in a fixed implementation language mapping $L$-programs to $M$-programs), composed sequentially. 2-cells $\alpha : t \Rightarrow t'$: *equivalence witnesses*, i.e. traces of program transformations relating $t$ and $t'$ whose endpoints are semantically equal. Vertical composition concatenates traces; horizontal composition whiskers by translation. The pattern follows Seely [8]: 1-cells compute, 2-cells relate computations.
*Definition 3.* An interpreter for $L$ in $M$ is $\mathsf{int}$ with $[\![\mathsf{int}]\!]_M(p, d) = [\![p]\!]_L(d)$. A compiler $L \to M$ is a 1-cell $c$ with a correctness 2-cell $\kappa_c : \mathsf{run}_M \circ c \Rightarrow \mathsf{run}_L$.
*Open point.* Whether traces form a strict 2-category or only a bicategory (associativity up to trace rearrangement) depends on the trace calculus; settling this is milestone M2.
3. The projections as coherence
$$\text{(F1)}\; \mathsf{target} = [\![\mathsf{mix}]\!](\mathsf{int}, p) \quad \text{(F2)}\; \mathsf{comp} = [\![\mathsf{mix}]\!](\mathsf{mix}, \mathsf{int}) \quad \text{(F3)}\; \mathsf{cogen} = [\![\mathsf{mix}]\!](\mathsf{mix}, \mathsf{mix}).$$
*Observation 1.* Each projection is an instance of (PE), hence carries a canonical 2-cell: $\phi_1 : [\![\mathsf{target}]\!] \Rightarrow [\![\mathsf{int}]\!](p,-)$, $\phi_2 : [\![\mathsf{comp}]\!] \Rightarrow [\![\mathsf{mix}]\!](\mathsf{int},-)$, $\phi_3 : [\![\mathsf{cogen}]\!] \Rightarrow [\![\mathsf{mix}]\!](\mathsf{mix},-)$. Pasting $\phi_2$ with $\phi_1$ gives a compiler-correctness 2-cell $\kappa_{\mathsf{comp}}$.
*Observation 2.* If 2-cells are extensional (proof-irrelevant), any two parallel pastings coincide, so all routes to a correct compiler agree trivially. The content therefore lies entirely in intensional witnesses.
*Conjecture A (coherence).* For intensional witnesses, the two routes to a compiler—via $\phi_2$ directly, or via $\phi_3$ at $\mathsf{int}$ then $\phi_2$—are related by a 3-cell, and a specializer satisfying (PE) up to coherent witness induces a pseudo-algebra-like structure in which F2/F3 play the role of multiplication and its associator.
*Conjecture B (stabilization).* $\mathsf{cogen}$ is a fixed point up to renaming, $[\![\mathsf{cogen}]\!](\mathsf{mix}) \simeq \mathsf{cogen}$, and this is the categorical content of the tower stopping at F3. Glück's analysis of a possible fourth projection [9] is the operational evidence we will compare against.
4. Meta-circularity and JIT as reflection
Smith's reflective tower [6] runs level $n+1$ on an interpreter at level $n$.
*Definition 4.* A meta-circular structure on $L$ is an endo-1-cell $U : L \to L$ with a 2-cell $\varepsilon : U \circ \ulcorner-\urcorner \Rightarrow \mathrm{id}$ (reflection undoes reification). A JIT is a policy for replacing $U \circ \ulcorner p \urcorner$ by $\mathsf{target}_p$ along $\phi_1$.
*Definition 5.* Speculation with deoptimization is a *partial* 2-cell defined on a guard sub-object, with fallback to $U$; soundness requires guarded and fallback paths to agree on overlaps (the same gluing used in §5). Truffle realizes this by partial evaluation of self-specializing AST interpreters [3,4]; PyPy by tracing the interpreter loop [5].
*Observation 3.* The tower collapses when $U$ is specialized away at level 1: this is F1 with $\mathsf{int} = U$.
5. Distribution over untrusted nodes
*Definition 6.* A residual program presents a dataflow wiring diagram in Spivak's operad of wiring diagrams [10]. A network is a site $N$: objects are nodes and coalitions, arrows inclusions. Placements form the Grothendieck construction $\mathcal{P} \to \mathcal{W}$ of the functor sending a decomposition $w$ of the diagram to assignments of its boxes to $N$; refining a decomposition reindexes.
*Definition 7 (trust presheaf).* For a coalition $U$, $\mathcal{V}(U)$ is the set of results of boxes placed in $U$ that are *verifiable* from $U$'s outputs: carrying an interactive or succinct proof [11,12,13], a hardware attestation [14], or a Byzantine-agreement certificate [15]. Restriction forgets boxes.
*Conjecture C.* For a coverage matching the trust model (e.g. covers of size $\ge 2f+1$ under $f$ Byzantine faults), $\mathcal{V}$ is a sheaf, and failure of gluing—locally consistent results with no global section—localizes a lying coalition, in analogy with the Abramsky–Brandenburger sheaf treatment of contextuality [16].
*Definition 8 (cost).* Enrich $\mathcal{P}$ over Lawvere's quantale $([0,\infty], \ge, +)$ [7]: hom = migration cost. Each deployment has intrinsic cost $c(x)$ = compute + communication + verification, where verification depends on the certifying method (replication, proof, attestation).
*Problem.* Minimize $c(x)$ over deployments that carry a global section of $\mathcal{V}$, under latency bounds.
*Conjecture D (non-commutation).* Specialize-then-decompose and decompose-then-specialize differ by a 2-cell whose cost is the lost cross-box optimization; optimal schedulers must search both orders.
*Observation 4 (verifiers by Futamura).* A verifier for a box is a program; specializing a generic verifier to the box is F1. The same cogen therefore yields verifier generators, so agent-built specializers amortize verification as well as speed.
6. Planned artifacts and milestones (future work)
Nothing below exists yet. Each milestone ends with a public, scripted, reproducible release.
- **M1 — A1
Fut0(weeks 1–2).** First-order functional language (integers, pairs, conditionals, first-order recursion), s-expression syntax, Python definitional interpreter (~300 lines), property-test harness. - **M2 — A2
mix0(weeks 3–6).** Offline partial evaluator with binding-time analysis and polyvariant specialization, written inFut0so it is self-applicable. Deliverables: F1 tests against the interpreter; F2 producing a compiler for a tiny stack language; an F3 attempt with sizes and timings; transformation traces exported as 2-cell witnesses, used to test Conjectures A and B on examples and to settle the strict vs. bicategorical question. - M3 — A3 meta-circular runtime (weeks 7–8).
Fut0interpreter inFut0; toy JIT that after $n$ calls with equal static arguments invokesmix0and caches guarded residual code with fallback (Definition 5). - **M4 — A4
place0scheduler (weeks 9–12).** Input: residual dataflow DAG and a network model (link costs; nodes honest, Byzantine, or attested). Output: minimum-cost deployment with per-box certification by $k$-replication or probabilistic re-execution. Exhaustive search to 10 boxes, then ILP/greedy. A gluing pass reports the minimal inconsistent coalition (Conjecture C). Simulated adversarial nodes. - M5 — A5 evaluation and full manuscript (weeks 13–16). (i) projection correctness; (ii) cost of the two orders in Conjecture D; (iii) detection rate and overhead vs. Byzantine fraction. Succinct proofs are only cost-modelled from published asymptotics, not integrated.
7. Expected failure points
- Real specializers are partial; (PE) holds only on terminating inputs, so $\mathcal{L}$ should be enriched in partial maps or domains.
- Observation 2 means the programme stands or falls on a precise intensional witness calculus.
- Conjecture C assumes a fixed coverage; dynamic membership and Sybil attacks break it.
- The agent-productivity hypothesis is empirical; M1–M4 are a first, small test.
mix0is far from Truffle-scale specialization of higher-order effectful languages [3,4].
References
[1] Y. Futamura. Partial evaluation of computation process—an approach to a compiler-compiler. *Systems, Computers, Controls* 2(5), 1971. Reprinted in *Higher-Order and Symbolic Computation* 12(4):381–391, 1999. doi:10.1023/A:1010095604496
[2] N. D. Jones, C. K. Gomard, P. Sestoft. *Partial Evaluation and Automatic Program Generation.* Prentice Hall International, 1993. ISBN 0-13-020249-5. https://www.itu.dk/~sestoft/pebook/jonesgomardsestoft-a4.pdf
[3] T. Würthinger, C. Wimmer, A. Wöß, L. Stadler, G. Duboscq, C. Humer, G. Richards, D. Simon, M. Wolczko. One VM to rule them all. *Onward! 2013*. doi:10.1145/2509578.2509581
[4] T. Würthinger, C. Wimmer, C. Humer, A. Wöß, L. Stadler, C. Seaton, G. Duboscq, D. Simon, M. Grimmer. Practical partial evaluation for high-performance dynamic language runtimes. *PLDI 2017*. doi:10.1145/3062341.3062381
[5] C. F. Bolz, A. Cuni, M. Fijałkowski, A. Rigo. Tracing the meta-level: PyPy's tracing JIT compiler. *ICOOOLPS 2009*. doi:10.1145/1565824.1565827
[6] B. C. Smith. Reflection and semantics in Lisp. *POPL 1984*. doi:10.1145/800017.800513
[7] F. W. Lawvere. Metric spaces, generalized logic, and closed categories. *Rend. Sem. Mat. Fis. Milano* 43:135–166, 1973. doi:10.1007/BF02924844
[8] R. A. G. Seely. Modelling computations: a 2-categorical framework. *LICS 1987*, 65–71. https://lics.siglog.org/1987/Seely-ModellingComputatio.html
[9] R. Glück. Is there a fourth Futamura projection? *PEPM 2009*. doi:10.1145/1480945.1480954
[10] D. I. Spivak. The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits. arXiv:1305.0297, 2013.
[11] S. Goldwasser, Y. T. Kalai, G. N. Rothblum. Delegating computation: interactive proofs for muggles. *STOC 2008*. doi:10.1145/1374376.1374396
[12] B. Parno, J. Howell, C. Gentry, M. Raykova. Pinocchio: nearly practical verifiable computation. *IEEE S&P 2013*. doi:10.1109/SP.2013.47
[13] E. Ben-Sasson, I. Bentov, Y. Horesh, M. Riabzev. Scalable, transparent, and post-quantum secure computational integrity. IACR ePrint 2018/046. https://eprint.iacr.org/2018/046
[14] V. Costan, S. Devadas. Intel SGX explained. IACR ePrint 2016/086. https://eprint.iacr.org/2016/086
[15] M. Castro, B. Liskov. Practical Byzantine fault tolerance. *OSDI 1999*. https://www.usenix.org/conference/osdi-99/practical-byzantine-fault-tolerance
[16] S. Abramsky, A. Brandenburger. The sheaf-theoretic structure of non-locality and contextuality. *New J. Phys.* 13:113036, 2011. doi:10.1088/1367-2630/13/11/113036