Open Research Directions

PFCL language reference · composure.systems

The other pages on this site specify what PFCL does. This page is different: it states questions PFCL's design has surfaced but not answered, for anyone who wants to work on them. Each item below is a real gap, not a rhetorical one — where an answer would change something in the implementation, that's said explicitly, and where the current state is a placeholder rather than a result, that's said too. This page assumes familiarity with the mechanisms described at /catalog, /identity, /catalog/equivalence, and /execution-hosts — read those first if a term here is unfamiliar.

None of these require access to anything private. Everything referenced is on this site or in the public PFCL repository.

1.Is there a unified formal treatment of identity, naming, and equivalence as separate relations?

/identity specifies PFCL's design commitment: identity, naming, and equivalence are three distinct relations, deliberately kept apart rather than conflated the way most systems conflate at least two of them. The justification given there is informal — an argument by cases (the ladder argument for why identity stays intensional) and a set of consequences (no diamond dependencies, no avalanche on rebind) rather than a theorem. Each relation individually has some formal footing — identity is exact syntactic equality, about as simple as a relation gets; equivalence is specified as a graded family of increasingly coarse relations in /catalog/equivalence; naming is a mutable partial function from names to identities. What doesn't exist is a treatment of the three together, as one coherent mathematical structure, with properties proven about how they interact rather than asserted by design narrative.

The open question, concretely: is there a formal algebraic or categorical structure that captures all three relations and their interactions — for instance, characterizing identity as the discrete (finest possible) equivalence on canonical syntax, naming as a partial function into that space that may change over time, and the equivalence ladder as a chain of increasingly coarse relations refining toward, but never reaching, semantic equality? Are there properties one would want to prove about this structure — does resolving a name to its current identity ever need to interact with an equivalence judgment (for instance, if two identities are judged equivalent at some grade, does that constrain which one a name is "allowed" to point to, or are the two completely independent as currently designed)? Is the current design's independence between naming and equivalence actually the right choice, or does it leave something on the table?

Where this connects to existing literature, unexplored so far: lambda-calculus equality notions (alpha/beta/eta, and the distinction between definitional and propositional equality in type theory) bear directly on where PFCL's identity/equivalence boundary is drawn. Content-addressing and cryptographic identity have their own literature, mostly from distributed systems and version control, largely disconnected from the type-theoretic equality literature — PFCL's design sits at the intersection of both and hasn't been positioned against either rigorously. Nominal sets and nominal logic (Gabbay–Pitts and the line of work following it) are a specific, concrete pointer worth flagging: that literature exists precisely to reason formally about names and binding while keeping identity syntactic, which is close to what PFCL's design does informally by refusing to fold alpha-equivalence into identity — see /catalog/related-work/unison §2 for the concrete system (Unison) that makes the opposite choice. Naming systems literature more broadly (from DNS to capability-based naming) is a third relevant thread, essentially untouched here so far.

This is likely the least tractable item on this page precisely because it's the least implementation-shaped — it's a question about whether a coherent theory exists, not about whether a mechanism can be built. It's also, for the same reason, the item where literature review rather than engineering is the actual bottleneck.

2.Is the state/capability duality the right split?

PFCL's type system treats two kinds of composition differently, on purpose. A function's state — the record shape it threads through a computation — is open row-polymorphic: {count: Int | r} matches any record carrying a count field, ignoring the rest, and this is how independently-written handlers compose without needing to know about each other's fields. A function's capability — the set of effect kinds it may emit — is deliberately closed: computed by a bottom-up fold over a function's body, checked at build time against a fixed, cemented envelope, with no row variable on that side at all.

The argument for the asymmetry: a PFCL value has a fixed body, therefore a fixed effect footprint, therefore higher-rank effect polymorphism has nothing to range over — there's no variable-effect-set position for a row to abstract over in a language where a function's emissions are a computable property of its own definition, not a parameter. Row polymorphism is kept where openness is real (state composition varies genuinely across contexts) and rejected where it would be pure unused machinery (capability sites resolve exactly, once, at the fold).

The open question: is this argument actually complete? It's an argument from PFCL's own totality and purity guarantees, and it may not generalize, or it may generalize further than currently claimed. A few concrete sub-questions: does the argument still hold once first-class effect-polymorphic combinators are considered (a function parameterized over which handler it composes with, rather than over its own body)? Is there a formal characterization of exactly which effect systems this argument applies to, versus systems like Koka or Frank where the row-polymorphic effect typing is doing real work? A careful treatment would need to relate this to the algebraic-effects literature (Plotkin–Power, Plotkin–Pretnar) properly, which hasn't been done rigorously here.

Current status: the split is implemented and load-bearing in the event loop's design; the argument for why it's correct is stated in design documentation, not independently reviewed or formalized. One piece of it is more concrete than the rest and worth isolating: the closed side is implemented as an actual algebraic structure, not just a fixed set — providers compose as a monoid (provider_A ⊕ provider_B, with the envelope composing as literal set union), and the single-provider, bound-at-construction discipline is what makes the loop's output a pure function of its event history at all — a dynamically attached provider would reopen exactly the closed world that guarantee depends on. Whether this composition genuinely satisfies the monoid laws (associativity, a verified identity element) hasn't been checked formally; it's asserted by construction, not proven. See section 6 for a related, more precisely scoped question about the boundary this envelope protects.

3.Distributed proof across independently-compiled trust boundaries

A running PFCL system spans two domains that are never compiled or checked together: the PFCL side (trusted by construction — totality, purity, and content-addressing hold by the type checker's own guarantees) and a host executor (trusted by whatever tool verifies it — deductive verification, bounded model checking, or nothing at all, depending on the host). The two are joined at one seam: a handler emits a list of command records; the host performs them and, where relevant, injects a reply. Today, that seam's existence and permission property (did the handler only emit commands the host is willing to perform) is checked statically and holds universally. But the seam's shape agreement property — does the host's reply actually carry what the PFCL side expects it to carry — is verified only by tests run against specific, exercised paths. It's an existential guarantee, not a universal one.

Because PFCL's totality means a shape mismatch at this seam doesn't crash — the reply parser is itself total, so a mismatch quietly falls through to a default value rather than failing loudly — this gap has a real, silent failure mode rather than a merely theoretical one.

The open question: can this last joint be upgraded from existential to universal without a single checker spanning both sides — which can't exist, since the two sides may be compiled separately, in different languages, for different processes? The proposed direction is assume-guarantee composition over content-addressed proof certificates: each side proves a property conditional on an assumption about the other, and the two proofs compose into an unconditional guarantee without either side's checker ever seeing the other's code. A first concrete primitive in this direction — a termination certificate, content-addressed and independently checkable — already exists and works. The general scheme for composing certificates across a seam like this one is not built, and turning "a termination certificate can be checked independently" into "an arbitrary shape-agreement property can be proven this way, compositionally, across any two domains that never see each other's source" is the actual research problem. This connects to existing work on assume-guarantee reasoning and certified compilation, but the specific shape here — independently-compiled domains joined by a runtime message-passing seam, verified by heterogeneous tools on each side — doesn't map cleanly onto any one existing framework as far as current investigation has found.

Two structurally different gaps hide inside "verify the seam," worth naming separately because they respond to completely different kinds of effort. Call them Gap A and Gap B. Gap A is whether an implementation's interface behavior — the shape and sequencing of what it sends and receives — matches its own stated contract. This is narrowable by ordinary means: richer types, session types (section 6), SMT within a decidable fragment, or composing proof-strength component contracts through ordinary Hoare-logic composition ({P} c1 {Q} and {Q} c2 {R} implies {P} c1;c2 {R} — textbook, and PFCL's absence of aliasing and mutation makes it a cleaner fit than most languages it was designed for). Gap B is whether the formal model itself — of a host's real behavior, of what a provider's OS or hardware actually does — corresponds to physical reality. No amount of narrowing Gap A touches Gap B, and this isn't a matter of insufficient cleverness; it's categorical. A proof relates one formal object to another formal object. Physical reality isn't a formal object, so nothing connects a proof to it directly — that connection is always trust, calibration, or empirical testing, never itself a proof.

This has real precedent even in the deepest verification work that exists. seL4 — the first machine-checked, full functional-correctness proof of a general-purpose OS kernel — states its own residual boundary directly in its abstract: "we assume correctness of compiler, assembly code, hardware, and boot code."[16] Even seL4's roughly 20 person-years of proof effort stops at the silicon. That boundary has real teeth: Meltdown and Spectre are cases where chips were formally specified to behave one way and the physical microarchitecture did something the formal model never captured (speculative execution leaking data through cache timing) — not a bug in any proof, a gap between the model any proof was relative to and what the hardware actually did. Software engineering has a name for exactly this split, usually attributed to Barry Boehm: verification ("are we building the product right" — does the implementation match the spec) versus validation ("are we building the right product" — does the spec correspond to reality).[17] A proof is always verification. It is never validation, and validation is understood in the formal-methods field itself as inherently empirical, not reducible to proof by any method, present or future.

One nuance worth being precise about, since it's easy to overstate the limit: a certified derivation — code produced through a machine-checked process (proof-assistant extraction, CompCert-style certified compilation) rather than hand-written and separately checked — genuinely can be proven to conform to its spec. That closes Gap A completely for whatever was derived this way. It says nothing about Gap B: the derivation is only ever as correct as the spec it started from, and no process, however rigorous, proves the spec itself is an accurate model of the real world. Bishop et al.'s decade-long formalization of TCP and the Sockets API in HOL is the clearest illustration of both halves at once — they formalized the spec rigorously, and then, for the conformance question, deliberately generated test oracles from it and ran them against real implementations empirically, rather than proving any real TCP stack correct.[18] That choice wasn't a shortcut; it's the only response available once a spec's correspondence to reality can't itself be proven.

4.The upper grades of the equivalence ladder

/catalog/equivalence specifies a five-grade ladder for recording that two distinct, non-identical catalog entries behave the same way. Grade 0 (exact-hash alias detection) ships today. Grades 1 through 5 — alpha-normalization, law-based equality saturation, SMT on a decidable fragment, bounded testing evidence, and full inductive proof — are specified in shape but not built, and several have open design questions with no committed answer:

• Grade 2 (equality saturation): what rule set earns admission, and by what criterion? A rule that's sound but rarely fires is dead weight; a rule that's unsound corrupts every judgment built on it. There's no stated methodology yet for admitting a rewrite rule to this set.
• Grade 3 (SMT): which fragment of the language is actually decidable in a way a solver can handle efficiently, and which encoding? This is a real scoping problem, not just an engineering one.
• Grade 4 (bounded evidence): given that PFCL is total and every function's input domain is fully representable, is there a principled way to choose a sampling strategy that gives meaningful bounded confidence, rather than an arbitrary one? What does "enough samples" mean for a function whose domain, while total, may still be enormous?

A related, sharper question: is the admission process itself confluent — do near-duplicate functions submitted in different orders collapse to the same equivalence classes regardless of order, once a grade-1 normalizer exists? This is a concrete, checkable claim (a permutation stress test against a fixed near-duplicate set) once grade 1 ships, and nobody has run it yet.

5.Formalizing what it means for a host to conform

/execution-hosts and /effects-as-data describe the contract between a PFCL function and a host: a host is any program that reads command records and performs the actions their kind field names. This is stated informally — "reads records and performs actions on their kinds" — and demonstrated by example (several drivers, from a one-shot batch runner to a full scheduled event loop, all driving the same pure step), rather than specified as a checkable property.

The open question: is there a decidable, checkable notion of host conformance — something closer to a type or a contract a host implementation could be verified against, rather than a prose description a host author has to interpret correctly by hand? If so, what does it look like, and is it strong enough to catch the failure mode in section 3 above (a host that reads a command correctly but replies with the wrong shape) before it becomes a runtime problem? This sits at the intersection of section 3 and this section: a formal host-conformance notion would be a natural place to attach the assume-guarantee scheme's "assumption" half for the effect-boundary seam specifically.

6.Is there a checkable protocol for the exchange over time, not just per-message shape?

Section 5 asks about the shape of one command and one reply. There's a sharper version of the same question: /execution-hosts rung 3 already has an implicit sequencing rule, not just a shape rule — a request carrying a correlation tag must be answered by its matching completion before certain follow-on inputs make sense, and a host that replies to the wrong request, or replies twice, or never replies, breaks something that no single message's shape-check would catch. This is a protocol in the precise technical sense used in concurrency theory: a constraint on the legal sequence of exchanges between two parties, not just on any one message in isolation. Right now this constraint exists only as prose in the design documentation and as whatever a host author infers from reading it.

The open question: can the exchange between a PFCL program and a host be given a type in the sense the session-types and typestate literatures use the word — a description precise enough that a checker, rather than a careful reader, can verify a host honors the sequencing it's supposed to? Two established lines of work look directly relevant and neither has been applied here yet:

• Session types, originating with Honda's dyadic interaction types[9] and the structured communication-based programming line of work that followed,[10] type a two-party exchange as a whole — the sequence of sends and receives each side is committed to, not just each message's payload type. Multiparty session types[11] extend this to more than two participants communicating over a shared protocol, which is the relevant extension once a program has more than one live input source (execution-hosts rung 4 and above) rather than the single request/reply channel rung 3 describes.
• Typestate, originating with Strom and Yemini,[12] types a single stateful entity's legal next operations as a function of its current state — closer to describing, from the host's own side, which command kinds are sensible to expect or emit given where a correlation-tagged exchange currently stands, independent of who's on the other end.

Neither framework has been checked against PFCL's actual command/reply shapes to see whether either fits cleanly, whether some combination is needed, or whether the correlation-tag mechanism as currently specified resists being typed this way for a reason not yet identified. This connects to sections 3 and 5 directly: a session-typed or typestate-checked protocol description would be a natural, formal shape for the "assumption" half of the assume-guarantee scheme in section 3, and a stronger, more precise answer to the host-conformance question in section 5 than a purely structural per-message check can give on its own.

A concrete, smaller worked example exists already, at the Composure event-loop level rather than the standalone-host level. The IoProvider boundary — poll(timeout_ms) -> Vec<Event> and execute(command) -> Vec<Event> — is a two-role exchange with strictly non-overlapping responsibilities: the provider only ever originates events, the loop only ever originates commands, and execute's own return type already carries "immediate follow-up events," the same request/completion shape rung 3 describes at the standalone level. This is small and precise enough to be a tractable first case for either framework above, rather than starting directly with the larger, less-specified standalone host contract.

What formalizing this specific boundary would and wouldn't buy is worth separating precisely, because it splits cleanly along the Gap A/Gap B line from section 3. A session type over poll/execute could catch dropped or duplicated correlation tags, out-of-order completions, or an event kind the loop never declared expecting for a given command — properties of the interface that nothing in the host language's own type system currently checks, since Vec<Event> typechecks regardless of whether the tags inside it are correct. This is Gap A, and it's a real, checkable narrowing of exactly the existential-vs-universal shape-agreement problem named in section 3. It does not touch Gap B — whether the underlying effect actually happened as claimed. A provider can satisfy a session type perfectly (correct tag, correct order, correct shape) while silently failing to perform the real-world action a command described. That's the same gap the project's own L9 principle already targets by a different, non-proof route (live wire validation, since a mock can't surface a race that only a real interaction exposes), and no protocol-typing approach closes it — per section 3, it's bound by the same limit as everything else on the Gap B side: either compose with an already-verified component, spend real verification effort on the highest-stakes provider specifically, or keep narrowing confidence through testing without ever reaching proof.

7.Admission governance as a synthesis-precision trade-off, generalized

PFCL's catalog admits or refuses candidate entries against structural rules beyond simple type-correctness — see /catalog/governance. One concrete instance: open row-polymorphic signatures are governed at admission (denied by default, allowlisted per namespace when justified) because a wide signature matches more record shapes than a narrow one, which widens what a search over the catalog returns for a given query — useful for the signature's own composability, costly for anyone else's search precision. This is currently handled as a targeted lint with a bounded-match-set threshold, decided case by case.

The open question: is there a general, principled way to characterize this trade-off — something closer to a formal cost function relating a signature's generality to its effect on catalog-wide search precision — rather than a per-mechanism lint rule decided independently each time a new kind of generality (row polymorphism today, potentially higher-kinded types or similar in the future) shows up? A real answer here would generalize past row polymorphism to any future admission-governance decision with the same shape, rather than requiring a new bespoke rule each time.

8.Is content addressing a prerequisite for composition, or merely a very effective choice?

Everything else on this site treats content addressing as a design decision that pays off — fewer conflicts, cheaper caching, verifiable identity. There's a stronger claim sitting underneath that framing, worth stating and questioning directly rather than leaving implicit: that a set of functions and the relation of what composes with what is a genuine mathematical object — independent of the syntax it happens to be written in — and content addressing is what gives that object a stable coordinate system to be referred to by. On this view, a name-based or mutable-identity system isn't just more prone to conflicts; it never quite manages to point at the composition relation itself, only at whatever currently happens to sit behind a name at a given moment.

The open question: is this actually true, or is it an evocative but unproven framing? Compositionality has a precise, older meaning in logic and semantics — the meaning of a whole is a function of the meanings of its parts and how they're combined — and a substantial literature exists on what's required for a system to have that property cleanly, both in the classical denotational-semantics sense and in the more recent categorical treatment of compositional structure generally.[14] None of that literature, as far as current investigation has found, makes content-addressed identity a necessary condition for compositionality in this formal sense — it's entirely possible to point at a counterexample: a system with mutable, name-based identity that is still compositional in the classical sense (the meaning of f(g(x)) is still a function of the meanings of f and g), provided nothing changes out from under a running composition mid-evaluation. What content addressing more clearly buys is something weaker but still valuable and worth stating precisely instead of conflating with compositionality itself: referential stability across time — the guarantee that a composition, once formed, continues to refer to the same parts indefinitely, regardless of what happens elsewhere in the system. A sharper version of the open question, then: is referential stability across time actually required for compositional reasoning to scale to a large, multi-author system in practice, even though it isn't required for compositionality to hold in the narrow formal sense at any single instant? If so, is there a proof of that — something showing name-based systems necessarily accumulate a specific, characterizable failure mode as scale grows, rather than an empirical observation (dependency hell exists, diamond conflicts happen) standing in for a proof that they must?

A careful treatment of this would need to engage the classical compositionality literature and the categorical treatment of composition directly,[13] rather than relying on the intuitive framing given above, which is suggestive rather than rigorous. It would also need to confront whether "necessary" is even the right word to reach for, or whether the right conclusion is that content addressing is one sufficient mechanism among several for a weaker, still-valuable property, and the interesting research contribution is characterizing that property precisely rather than defending content addressing's necessity.

9."Composition" is at least three different properties, usually treated as one

Section 8 asks whether content addressing is necessary for compositionality. That question presupposes "compositionality" is one thing. It probably isn't, and the conflation is worth naming as its own open question, because PFCL's own guarantees answer some of the three senses below cleanly and say nothing at all about the others.

Algebraic composability. Can two functions even be combined, and does the operator combining them behave well as an algebra — associative, with identities, obeying stated laws. This is what the algebra-of-programs tradition (Backus's combining forms,[19] the Bird–Meertens calculus, the recursion-scheme operators of Meijer–Fokkinga–Paterson[20]) establishes. It is a structural question about the operation of composing, answerable without reference to what either function actually computes.

Denotational compositionality. Given that f and g can be combined, is the meaning of the combination determined purely by the meanings of f and g, with nothing else needed — does ⟦f∘g⟧ reduce cleanly to a function of ⟦f⟧ and ⟦g⟧ alone. This is not automatic once effects enter the picture. Moggi's own motivation for introducing monadic semantics was exactly this failure: naive equational reasoning "identifies programs with total functions from values to values,"[15] which stops correctly describing composition once evaluation order, effect timing, or partiality can make ⟦f∘g⟧ depend on more than the two meanings in isolation. A monad is machinery for recovering compositionality once it would otherwise break.

Specification correctness. Given that f∘g is well-formed and its meaning is cleanly determined, does that meaning match what the composer actually intended. This is not guaranteed by either of the first two properties — two functions can compose with perfect algebraic and denotational cleanliness and still build the wrong system, because a type signature is a coarse proxy for intent. This sense of "composes correctly" belongs to specification and verification (contracts, refinement, Hoare-style reasoning) rather than to the algebra-of-programs literature at all.

Where PFCL's own guarantees actually land, stated precisely rather than implied: totality and purity give the second property, denotational compositionality, close to automatically — because every PFCL function terminates and has no hidden effects, ⟦f∘g⟧ is determined by ⟦f⟧ and ⟦g⟧ without needing Moggi's monadic bookkeeping to patch around effect ordering, since there's no effect ordering to patch around. This is a real property, earned by the totality and purity guarantees specified elsewhere on this site, not an assertion. It says nothing, however, about the third property. Nothing about totality or purity implies a given composition means what its author intended; that gap is exactly what the upper grades of /catalog/equivalence (SMT, bounded evidence, inductive proof) are reaching toward, from an angle — verifying behavioral equivalence between existing entries — that's adjacent to but not identical to verifying a new composition against its author's actual specification.

The open question: is this three-way decomposition the right one, or does it collapse under scrutiny — is denotational compositionality actually a special case of specification correctness (a very weak specification: "means something, determined by the parts"), rather than a genuinely separate tier? And is there a way to state what PFCL's totality and purity guarantees buy, precisely, in terms that connect directly to the classical compositionality literature (Janssen, Montague) rather than to the informal argument given above? A rigorous treatment would need to formalize each tier and show, rather than assert, that PFCL's guarantees place it where this section claims.

Contributing

None of the above is blocked on anything other than the work itself. The relevant design documents, where they exist beyond what's summarized here, and the catalog and type-checker implementation, are in the public PFCL repository. If you work on any of these and want to discuss it, the repository's issue tracker is the right place — or get in touch directly.