Analysis of both papers against the current rlm-scheme implementation, ROADMAP, referenced PL papers, real-world usage report, and four sub-model expert analyses (PL theory, AI/ML research, formal methods, systems architecture) conducted via the rlm-scheme tool — 5 sub-model calls, ~18K tokens, parallel fan-out across 4 analysis dimensions.
Two rounds of analysis:
- V1: Manual gap analysis comparing papers to implementation, ROADMAP, and referenced PL literature.
- V2: rlm-scheme-assisted analysis with 4 parallel expert sub-model calls (PL theory, AI/ML, formal methods, systems architecture) + synthesis.
This file is the combined result. Items are organized by paper, then by category.
The paper describes a proof-of-concept Python testbed (~300 LOC) and frames real Scheme runtime integration as future work (§6.1). The actual codebase is now a fully working Racket sandbox + MCP server (~2100 LOC) with 211 passing tests. This is the single largest gap: the paper undersells what now exists.
The paper's §6.1 lists four "key implementation steps" as future work:
| Paper §6.1 says... | What actually exists |
|---|---|
| "Racket subprocess server (~200 LOC)" | racket_server.rkt — 824 lines, full sandbox |
| "Bridge client (~100 LOC)" | mcp_server.py — 1157 lines, MCP server + call registry |
| "LM handler integration" | OpenAI API integration with model routing |
| "Restricted grammar enforcement" | Sandbox blocks set!, call/cc, define-syntax, I/O |
Action: Rewrite §6.1 as an implementation report. The four steps are done.
Show the architecture diagram from the README (Claude Code → mcp_server.py → racket_server.rkt → py_bridge.py) and discuss what was learned building it.
Move remaining future work (formal verification, static types) to a new §6.x.
| Metric | Paper claims | Current state |
|---|---|---|
| Test count | 83 (59 deterministic + 24 comparative) | 211 across 6 files |
| Test categories | 4 failure categories | 6 files: core eval, hygiene, MCP server, callbacks, recursion, API params |
| Implementation | Python testbed simulating Scheme API | Real Racket sandbox with actual shift/reset |
| Scheme-path tests | 24 comparative (Python vs Scheme mock) | 26 adversarial hygiene tests against real sandbox |
Action: Update Tables 3 and 3b. The narrative can now say "the same adversarial scenarios from the Python testbed all pass in the real Racket sandbox, confirming that language-level guarantees replace convention-level ones."
The README's comparison table has features the paper doesn't mention:
| Feature in README | Paper coverage |
|---|---|
llm-query-async + await (parallel fan-out) |
Mentioned in §4.5 as "preview"; now implemented and tested |
#:image / #:images (vision) |
Not mentioned at all |
#:json #t (structured JSON output) |
Not mentioned |
py-set! (safe data transfer) |
Not mentioned — only py-exec/py-eval are in Appendix C |
Token budget via parameterize |
Mentioned in §3.5; now implemented with real API token counts |
Call registry + cancel_call |
Not mentioned |
| Crash recovery + auto-restart | Not mentioned |
get_token_usage MCP tool |
Not mentioned |
Recursive delegation (#:recursive #t) |
Mentioned conceptually; now implemented with nested sandbox lifecycle |
Action: Expand §4.2 and the scaffold reference (Appendix B) to cover these. The vision and JSON mode features are especially significant — they extend scope hygiene to new modalities.
The #:image/#:images support creates a new scope boundary type not
discussed in the paper. When a sub-model receives both text and images, the
provenance tracking must cover two modalities:
- Text data has scope marks from syntax objects
- Image data has no equivalent scope annotation
This creates an asymmetry: a sub-model's response might be influenced by an injected image (visual prompt injection) that the scope log doesn't track at the same granularity as text injection.
Idea: Extend the scope log to record image provenance — which images were
sent to which sub-call, at what resolution, from what source. The _resolve_image
method in mcp_server.py already validates images (magic bytes, size limits);
this metadata could feed into the scope log.
PL analogy: This is the multi-sorted algebra version of scope hygiene — the original Kohlbecker (1986) system handles one sort (identifiers); extending to images is extending to a second sort with different scope rules.
The usage report (rlm-scheme-usage-report.md) identifies py-set! as solving
"the most frustrating ergonomic issue" — escaping conflicts when passing Python
regex patterns through Scheme string literals. This is a real-world discovery
that validates Matthews and Findler (2007) multi-language semantics:
py-execembeds Python code as a string in Scheme — a Scheme-level value containing Python-level syntax. Escaping conflicts are the same problem as unhygienic interpolation, just at the inter-language boundary.py-set!sends data as JSON over a pipe — a proper boundary term that marshals values between type systems without embedding one language inside another.
Idea: Add a subsection to §4.2 or §7 showing that the
orchestration/computation boundary suffers from the same scope problems as the
orchestration/sub-LLM boundary, and py-set! is the analogue of datum->syntax
for the Python layer.
The _active_calls registry in mcp_server.py tracks every in-flight sub-model
call with: call_id, type (sync/async/recursive), model, depth,
instruction_preview, parent_id, start_time, future, nested_repl, cancel_event.
This is an expansion trace — the term used in §2 and Table 1's "Also Enables" column. The paper claims syntax objects enable expansion traces; the implementation delivers them via the call registry. This should be presented as evidence that the "Also Enables" predictions from Table 1 are materializing.
Concrete data point: The usage report shows 8 LLM calls across 3 parallel branches for 15 papers, all tracked in the scope log. The audit trail let the user "verify that every paper was actually processed."
Frame the entire scaffold as an algebraic effect system (Plotkin and Pretnar 2009, Bauer and Pretnar 2015):
llm-queryis an effect: "I need a sub-model response"- The MCP server is the handler: it interprets the effect by calling the OpenAI API
unsafe-raw-queryis the same effect with a different handler that skips scope wrappingunsafe-overwriteis a state effect with a privileged handler- Token budgets are a resource effect with a decrementing handler
llm-query-asyncvsllm-query= shallow vs deep handlers (Hillerstrom and Lindley 2018)
This provides a cleaner unifying framework than treating each primitive separately. The effect signature:
effect LLMQuery : Instruction * Data * Model -> ScopedResponse
effect PyExec : Code -> String
effect Finish : Value -> Empty
effect Unsafe : UnsafeOp -> Value
References to add: Plotkin and Power (2003), Plotkin and Pretnar (2009), Bauer and Pretnar (2015) — "Programming with algebraic effects and handlers."
The syntax-object wrapping is a manual taint-tracking mechanism. Information flow type systems (Sabelfeld and Myers 2003; Jif language) formalize this:
- User data from
contexthas security levelLow(untrusted) - Scaffold instructions have level
High(trusted) llm-query #:instructionexpectsHigh;#:dataacceptsLowsyntax-eis a declassification — explicitly lowering the security level- Prompt injection is an implicit flow from
LowtoHigh
Novel idea: Reframe referential opacity (§3.3) using information flow
terminology. This connects to a much larger body of security literature and
strengthens the prompt-injection discussion in §7.3. The syntax-object mechanism
is a form of dynamic taint tracking — the same technique used in web security
(e.g., Perl's taint mode, Ruby's $SAFE).
Reference: Sabelfeld and Myers (2003) "Language-Based Information-Flow Security."
Apply blame theory (Wadler and Findler 2009) to the two-REPL boundary. When a scope
error occurs at the Scheme/Python boundary (e.g., a py-exec call returns data that
causes a scope violation when spliced into an llm-query), blame theory can attribute
the fault to the correct side of the boundary. The JSON bridge protocol is a contract
boundary; violations should produce blame labels indicating which language produced
the faulty value.
Concrete application: when py-exec returns a string that contains instruction-like
text and this string is passed to llm-query #:data, the scope system can attach
blame to the Python side (the data source) rather than the Scheme side (the
orchestration). The _active_calls registry already tracks call provenance; blame
labels would formalize this.
Reference: Wadler and Findler (2009) "Well-Typed Programs Can't Be Blamed."
The transition from Python's untyped f-string interpolation to Scheme's fully
scope-tracked llm-query is all-or-nothing. Gradual typing (Siek and Taha 2006)
suggests an intermediate path:
- Level 0: Raw string interpolation (current Python RLM)
- Level 1: Typed fields with runtime checks (
SubCallResultwrapper from the paper's Python testbed) - Level 2: Syntax objects with scope tracking (current Scheme layer)
- Level 3: Static type checking with phantom types (ROADMAP L2)
Each level adds guarantees. The gradual typing framing makes the adoption story
more compelling: users don't have to adopt everything at once. The unsafe-* escape
hatches are the "dynamic" portion of a gradual type system — they bypass static
guarantees with runtime logging.
Reference: Siek and Taha (2006) "Gradual Typing for Functional Languages."
The Racket-Python callback protocol (sandbox writes JSON request, blocks on stdin for response) follows a strict send-receive-send-receive alternation. This is a session type (Honda et al. 1998):
CallbackSession = !Request . ?Response . End
AsyncSession = !Request . End
AwaitSession = !AwaitReq . ?Response . End
The current implementation enforces this protocol informally (the Racket server
blocks on read-line after writing a callback). Session types would formalize the
protocol guarantee: the MCP server and Racket process are provably deadlock-free if
they respect the session type. This is especially relevant for async dispatch, where
the protocol is more complex (dispatch doesn't block, but await does).
Reference: Honda, Vasconcelos, and Kubo (1998) "Language Primitives and Type Discipline for Structured Communication-Based Programming."
The scope log records every sub-model call, every syntax-e unwrap, every unsafe-*
escape hatch. This audit trail is a natural training signal:
- Trajectories with fewer
unsafe-*calls are "cleaner" and should be preferred - Trajectories where
syntax-eis called before every string operation are "well-typed" - Trajectories that exhaust token budgets are "expensive"
A DPO (Direct Preference Optimization) setup could use scope traces to automatically rank trajectory pairs: the trajectory with better scope hygiene is preferred. This connects scope hygiene to the RLHF literature and suggests that the Scheme layer provides free training signal as a byproduct of its safety guarantees.
Current multi-agent frameworks (AutoGen, CrewAI, LangGraph) have no scope isolation between agents. When Agent A passes data to Agent B, there is no mechanism to track provenance or prevent capture. The syntax-object approach could extend to multi-agent systems:
- Each agent's outputs are wrapped in syntax objects tagged with the agent's identity
- Inter-agent communication preserves scope marks
- An agent that wants to interpret another agent's output as instructions must
explicitly
datum->syntax— a logged scope crossing
This positions the paper not just as an improvement to RLMs but as a foundational contribution to safe multi-agent orchestration.
The scope log provides an audit trail suitable for regulatory compliance:
- Healthcare: track exactly which patient data was sent to which sub-model, at what temperature, with what instruction
- Finance: demonstrate that trading signals were computed through a verifiable pipeline with no unauthorized data flow
- Legal: prove chain of custody for evidence processed through LLM pipelines
The get_scope_log MCP tool already provides this data. The paper could note that
scope hygiene has compliance implications beyond security.
The papers lack comparative benchmarks. Proposed experiments:
- Run the same adversarial inputs through LangChain, AutoGen, and rlm-scheme. Measure prompt injection success rates.
- Compare latency overhead: raw Python LLM calls vs. Scheme-orchestrated calls (the JSON pipe adds ~1ms; measure real-world overhead).
- Measure error rates: how often does each framework silently corrupt scope (namespace collision, delimiter capture) on standardized test inputs?
The papers/PLAN.md contains a detailed concept-by-concept DSPy comparison
(10-row table + 5 "looks like hygiene but isn't" items) that is far richer than
the current §7.3. Key points not in the paper:
- DSPy's
caller_modulesstack is "the closest thing to scope tracking in any mainstream LLM framework" but tracks which module is active, not where each datum came from - DSPy's
ContextVar-baseddspy.context()provides genuine dynamic scoping for settings but not for data provenance - DSPy's immutable-by-replacement signatures prevent cross-module mutation but not capture
- The two systems compose: DSPy optimizes prompt content, syntax objects track prompt scope
Action: Expand §7.3 with at least the layer diagram and the key insight about
caller_modules vs. data provenance. This strengthens the "complementary, not
overlapping" claim.
The usage report identifies three patterns from real-world use:
- Automated scan then targeted vision verification — regex/Python for breadth, LLM for depth judgment
- Categorize then batch-fix — Python categorizes, Python batch-applies
- LLM for judgment, Python for execution — the exact split §4.2 prescribes
Idea: Add these as empirical validation of the orchestration/computation separation in §4.2 or §7. They are not constructed examples — they emerged naturally from a user solving a real problem.
The mcp_server.py send() method catches RuntimeError, BrokenPipeError,
and OSError, kills the Racket process, restarts it, and returns an error
message suggesting the user reload context. This is structured backtracking
at the process level — the same capability §2 and Table 1 predict from delimited
continuations.
Idea: Note in §4.5 that crash recovery is a coarse-grained instance of the
structured backtracking that shift/reset enables at the fine-grained level.
Both let the scaffold recover from failures in the sub-computation.
§3.5 describes parameterize for token budgets as a theoretical mechanism. The
implementation has it working end-to-end:
token-budgetis a Racket parameter (make-parameter +inf.0)decrement-budget!checks and decrements on everyllm-query- Budget propagates to recursive sub-sandboxes via
_call_llm_recursive tokens-used-callbackqueries cumulative usage from the MCP server- The usage report shows 23,247 tokens consumed across a real task
Action: Add empirical token-budget data to §3.5 or §5. Show a concrete example
where a budget-exceeded error fired, demonstrating the mechanism prevents runaway
costs. The test_callbacks.py tests likely have examples.
The ROADMAP item L2 describes a concrete plan for static type checking:
Define a type grammar:
String,Scoped<s>,Number,Boolean,List<T>,Void. Write a type checker that walks the AST. Programs that pass today but are semantically wrong (e.g.,(string-append (llm-query ...) "x")) should fail at the type-checking stage.
This is exactly what §6.2 and the companion note predict: phantom types making scope violations compile-time errors. The ROADMAP makes this concrete enough to include as a "planned validation" in the paper.
Action: Reference the type grammar from L2 in §6.2, showing that the monadic framing's prediction (§5.1 of the companion note) has a concrete implementation path.
Appendix B lists 10 scaffold bindings. The implementation has 19+:
| In paper | Missing from paper |
|---|---|
llm-query, py-exec, py-eval, py-call |
llm-query-async, await |
finish, finish-var |
py-set! |
syntax-e, datum->syntax |
tokens-used, token-budget |
context |
#:image, #:images params |
unsafe-raw-query |
unsafe-interpolate, unsafe-overwrite, unsafe-exec-sub-output |
Action: Expand Appendix B to match the README's scaffold reference.
ROADMAP L1 describes integrating RLM-Scheme as a drop-in SchemeREPL(Environment)
for the upstream RLM benchmark. This would enable direct A/B comparison on
the original RLM benchmarks — the strongest possible validation. Even if not yet
implemented, describing the integration path strengthens §6.
The paper currently has a clean arc: identify bugs → map to PL theory → propose Scheme fixes → validate with testbed. The implementation adds a second act: build the real thing → discover new problems (escaping, crash recovery, vision) → solve them with the same PL principles. This validates the theory more strongly than the testbed alone.
Suggestion: Add a §5.4 or §6.1 subsection: "From Testbed to Implementation: What Changed." Cover: what the testbed predicted correctly (scope tracking works), what it missed (inter-language escaping, process lifecycle), and what the real implementation revealed (vision scope, call registry as expansion trace).
The companion note is purely theoretical — it describes monadic structure without referencing any implementation. The rlm-scheme codebase now provides concrete evidence for every claim:
| Note claims... | Implementation shows... |
|---|---|
return wraps a datum in a syntax object |
(datum->syntax #f result-text) in racket_server.rkt:480 |
bind is the dispatch-and-wrap step |
llm-query-callback → API call → datum->syntax in lines 469–480 |
finish is shift with empty continuation |
(shift k (finished-value val)) in line 416 |
| Filinski: any monad via shift/reset | The entire eval-top-level uses (reset expr) wrapping, line 719 |
Action: Add a §4b "Implementation Correspondence" showing these exact code locations. The monadic description and the Scheme implementation are provably the same structure.
The current table has 4 rows. Each can now be annotated with the test that validates it:
| Failure | Type Error | Test file | Test name |
|---|---|---|---|
| Delimiter capture | Tagged vs raw | test_hygiene.py |
test_finish_in_string_is_inert |
| Referential opacity | Untagged splice | test_hygiene.py |
test_prompt_injection_* |
| Namespace collision | Metadata corruption | test_hygiene.py |
test_redefine_scaffold_* |
| Cross-context breakage | A treated as Box A |
test_hygiene.py |
test_scope_log_* |
Action: Add test references to make the type-error claims empirically grounded.
The paper claims monadic structure but never states or checks the monad laws:
- Left identity:
return a >>= k = k a— wrapping a datum in a syntax object then immediately dispatching should equal dispatching directly - Right identity:
m >>= return = m— dispatching and re-wrapping should be identity - Associativity:
(m >>= k) >>= h = m >>= (\x -> k x >>= h)— chained sub-calls should be associative
State whether the implementation satisfies these laws. If it doesn't (e.g., because
datum->syntax adds scope marks that syntax-e strips — left identity might not
hold exactly), explain why the violation is benign or how it could be fixed.
The paper should clarify whether the orchestration operations form a Kleisli category.
Morphisms are a -> M b (functions that take a value and produce a monadic
computation). Composition is >=>: (f >=> g) x = f x >>= g. In the RLM:
f : String -> Scoped Stringmight bellm-query #:instruction "summarize"g : String -> Scoped Stringmight bellm-query #:instruction "translate"f >=> gis: summarize, unwrap, translate
Does Kleisli composition hold? This is where the scope marks might cause issues:
syntax-e strips marks, so g receives an unmarked string, not a Scoped value.
The composition f >=> g drops provenance at the junction point. This is a genuine
formal insight worth discussing.
The paper mentions continuations (Filinski) and monads (Moggi/Wadler) but doesn't specify which monad the RLM loop instantiates. It's actually a layered monad stack:
- Continuation monad:
finish/shift/resetprovide the control flow - State monad: the sandbox namespace is mutable state threaded through iterations
- Reader monad:
contextis a read-only environment available to all code - Writer monad: the scope log is an append-only trace
The interaction of these layers is the monad transformer stack. State this explicitly and discuss which transformers are needed and in what order.
parameterize + token-budget is not just a reader monad — it is a graded
monad (Katsumata 2014; Orchard et al. 2019). In a graded monad M_r a, the
grade r tracks a resource:
return : a → M_0 a— pure computation uses zero tokensbind : M_r a → (a → M_s b) → M_{r+s} b— sequencing adds token costsllm-query:M_k awherekis the token cost of the API callparameterize ([token-budget N]): imposes the constraintr ≤ N
The actual implementation tracks this: decrement-budget! sums costs, and errors
when the sum exceeds the bound. This is the operational semantics of a graded
monad with a budget constraint.
Novel contribution: Show that the token-budget mechanism is a graded monad. This connects the resource-threading concern (§3.5 of the main paper) to a formal framework and suggests static analysis: a type checker could infer worst-case token bounds by summing grades.
References to add: Katsumata (2014) "Parametric effect monads and semantics of effect systems"; Orchard, Wadler, and Eades (2019) "Unifying graded and parameterised monads."
llm-query (synchronous) = deep handler: the handler processes the effect and
resumes the computation. llm-query-async + await = shallow handler: the handler
returns a resumption (the async handle) instead of directly continuing.
This is the deep/shallow handler distinction from Hillerstrom and Lindley (2018).
Formalizing it explains why async dispatch doesn't need #:recursive support
(recursive calls require deep handling of the nested sandbox lifecycle, which
shallow handlers don't provide).
In effect systems, masking (Biernacki et al. 2019) allows an operation to
temporarily escape the current handler. The unsafe-* operations are exactly
this:
unsafe-raw-queryescapes the syntax-object handlerunsafe-interpolateescapes the scope-tracking handlerunsafe-overwriteescapes the module-protection handlerunsafe-exec-sub-outputescapes the sandbox isolation handler
Each is logged — this is the "evidence" requirement from effect-masking systems, where masked operations must produce an audit record.
Novel contribution: Frame the escape hatches as effect masking. This provides a principled taxonomy: each escape hatch corresponds to masking a specific effect, and the logging requirement corresponds to the evidence requirement in the theory.
_call_llm_recursive in mcp_server.py (lines 926–995) implements staged
computation literally:
- Stage 0: Build
full_instructionwithUSAGE_GUIDE— this isbracket - Stage 1: Call
_call_llm()to get Scheme code — this isrun - Stage 2:
_extract_code()parses the response — this isescape - Stage 3: Nested
RacketREPL.send()evaluates the code — this isrunagain
Each stage has a different evaluation context (the MCP server, the sub-LLM, the nested Racket sandbox). Cross-stage values (the instruction, the generated code, the result) pass through explicit boundaries.
Novel contribution: Walk through _call_llm_recursive as a concrete
instantiation of Taha and Sheard's bracket/escape/run. This makes the MetaML
correspondence concrete rather than analogical.
Matthews and Findler (2007) define boundary terms for multi-language programs.
The py-send! protocol in racket_server.rkt is a literal boundary term:
Scheme value → JSON serialization → pipe → JSON deserialization → Python value
The type coercion is explicit: Scheme strings become Python strings, Scheme lists become Python lists, syntax objects (no Python equivalent) raise errors. This is exactly the "natural embedding" from Matthews and Findler.
Novel contribution: Formalize the py-send! / py-set! protocol as a
boundary term. Show that py-set! eliminates the escaping problems because it
uses the natural embedding (JSON values), while py-exec with embedded strings
uses the lump embedding (opaque strings) — which is why it suffers from the
same scope problems as f-string interpolation.
The async dispatch protocol has coalgebraic structure:
- State:
{pending: Map<ID, Future>, active: Map<ID, CallMeta>} - Observations:
dispatch(id),await(id),cancel(id) - Transitions:
dispatchadds to pending;awaitblocks and removes;cancelremoves and kills
Model this as a coalgebra X -> F(X) where F captures the observable behavior.
The bisimulation relation between the Python thread pool implementation and the
Racket callback protocol proves behavioral equivalence.
Reference: Rutten (2000) "Universal Coalgebra: A Theory of Systems."
Scope transformations (wrapping with datum->syntax, unwrapping with syntax-e,
crossing with unsafe-interpolate) can be modeled as profunctor optics:
syntax-eis a getter (extracts the datum from a scoped value)datum->syntaxis a review (injects a datum into a scoped context)- The combined get/set behavior is a lens on the scope structure
This provides a compositional vocabulary for describing scope operations and could
enable optimization of scope-tracking pipelines (e.g., fusing consecutive
syntax-e/datum->syntax pairs).
Reference: Milewski (2017) "Profunctor Optics: The Categorical View."
Model evaluation contexts (GPT-5's interpretation context, Qwen3-Coder's context) as objects in a category, with morphisms representing context adaptation. Presheaves over this category capture how prompt meaning varies across contexts:
- A presheaf
P : Context^op -> Setmaps each model context to the set of meanings a prompt can have - A natural transformation
P -> Qrepresents a prompt adaptation that works uniformly across all contexts - Cross-context breakage is a failure of naturality
This connects Davies-Pfenning's modal types to a richer categorical framework.
The note is currently very compressed (97 lines). With the implementation evidence and novel ideas above, it could expand to:
- The Formal Structure (existing §1, expanded with implementation correspondence)
- Modal Types and Cross-Context Breakage (existing §2)
- Scope Failures as Type Errors (existing §3, expanded with test references)
- Why the Scheme Implementation Works (existing §4, expanded with code locations)
- The Monad Transformer Stack (new — F3 above)
- The Token Budget as a Graded Monad (new — F4 above)
- Async Dispatch and Effect Handlers (new — G1/G2 above)
- Implications for Future Work (existing §5, expanded with verified predictions)
The note introduces an assembly line analogy in §1 but drops it immediately. It could be a running thread: the graded monad is a budget attached to each station; the async dispatch is parallel assembly lines; the escape hatches are quality inspectors overriding the conveyor belt; blame = which station broke the product.
The note cites only 6 papers. With the novel ideas above, it should cite:
| New reference | For which idea |
|---|---|
| Katsumata 2014 | Graded monads (F4) |
| Orchard, Wadler, Eades 2019 | Graded/parameterised monad unification (F4) |
| Plotkin and Pretnar 2009 | Algebraic effects and handlers (B4, G1) |
| Hillerstrom and Lindley 2018 | Shallow vs deep handlers (G1) |
| Biernacki et al. 2019 | Effect masking (G2) |
| Matthews and Findler 2007 | Multi-language boundary terms (G4) |
| Sabelfeld and Myers 2003 | Information flow types (B5) |
| Wadler and Findler 2009 | Blame theory (B6) |
| Siek and Taha 2006 | Gradual typing (B7) |
| Honda et al. 1998 | Session types (B8) |
| Rutten 2000 | Coalgebra (G5) |
The note's §5 lists three future directions. The implementation has made progress on all three:
| §5 prediction | Current status |
|---|---|
| 1. Phantom types / static type checking | ROADMAP L2 has a concrete plan with type grammar |
| 2. Modal types for multi-model coordination | #:model per-call override exists; ROADMAP L5 plans vision-aware routing |
| 3. Formal verification of monadic laws | Not yet addressed, but 211 tests exercise the operational behavior |
Action: Add a "progress toward predictions" subsection showing that the theoretical directions are being pursued.
Compare the sandbox security model against:
- E2B: Cloud-based sandbox with network isolation — more flexible but external dependency
- Modal: Container-based isolation — stronger process isolation
- Firecracker: MicroVM-based — strongest isolation but highest overhead
- rlm-scheme: Racket sandbox (make-evaluator) with memory limit + blocked I/O — language-level isolation, lightweight, but relies on Racket's sandbox security
The paper should acknowledge that Racket's sandbox is not a security boundary in the
same sense as a VM or container — it prevents accidental misuse, not adversarial
escape. The unsafe-* operations are escape hatches by design.
Current architecture bottlenecks at scale:
ThreadPoolExecutor(max_workers=10)limits concurrent async calls- Nested REPLs for recursive calls each spawn a full Racket process
- JSON-over-stdin/stdout is single-threaded per Racket process
- The selector-based I/O (
selectors.DefaultSelector) handles one Racket process
For depth > 3 or 100+ concurrent calls, the architecture would need:
- Process pool for Racket instances
- Multiplexed I/O (e.g., Unix domain sockets with connection-per-call)
- Token budget aggregation across distributed workers
This is worth noting in §4.4 (Limitations) as an honest assessment.
The Racket-to-Python callback protocol (write JSON request to stdout, block on stdin for response, interleaved with eval results) is a novel IPC design worth formal treatment:
- It's deadlock-free by construction (each callback is a synchronous round-trip within a larger eval)
- It handles interleaved operations (eval continues between callbacks)
- It's naturally extensible (new callback ops like
tokens-usedadd one case each to both sides) - The async extension (dispatch without blocking, await later) breaks the strict alternation pattern safely
Session types (B8) formalize this. The protocol design pattern is reusable by other projects that need to embed foreign-language sandboxes.
| # | Item | Paper | Effort | Why |
|---|---|---|---|---|
| 1 | A1 | P1 | Low | §6.1 claims future work that's done — factual error |
| 2 | A2 | P1 | Low | Test counts are stale (83 vs 211) |
| 3 | E1 | P2 | Low | Ground claims in code locations — instant credibility |
| 4 | A3 | P1 | Medium | Missing 9+ features from the paper's scaffold reference |
| # | Item | Paper | Effort | Why |
|---|---|---|---|---|
| 5 | B4 | P1 | Medium | Algebraic effects unify the 4 primitives into one framework |
| 6 | B5 | P1 | Medium | Information flow types connect to security literature |
| 7 | F1 | P2 | Medium | Monad laws are the first thing a formal reviewer checks |
| 8 | F4 | P2 | Medium | Graded monads are the formal home for token budgets |
| 9 | D1 | P1 | Medium | DSPy comparison is currently too shallow |
| 10 | B2 | P1 | Low | py-set! validates Matthews-Findler — easy win |
| # | Item | Paper | Effort | Why |
|---|---|---|---|---|
| 11 | B6 | P1 | Medium | Blame theory for cross-language scope — novel |
| 12 | B7 | P1 | Medium | Gradual typing adoption story — practical |
| 13 | B8 | Both | Medium | Session types for callback protocol — novel |
| 14 | C1 | P1 | Medium | RLHF signal from scope traces — high impact if true |
| 15 | C2 | P1 | Medium | Multi-agent scope federation — positions paper broadly |
| 16 | F2 | P2 | Medium | Kleisli composition and provenance loss — genuine insight |
| 17 | F3 | P2 | Medium | Monad transformer stack — clarifies formal structure |
| 18 | G1 | P2 | Medium | Deep/shallow handlers for sync/async — clean formalization |
| 19 | G5 | P2 | High | Coalgebraic async protocol — mathematically rich |
| 20 | G6 | P2 | High | Profunctor optics for scope — novel but speculative |
| # | Item | Paper | Effort | Why |
|---|---|---|---|---|
| 21 | B1 | P1 | Low | Vision scope hygiene — implementation already exists |
| 22 | B3 | P1 | Low | Call registry as expansion trace — easy section |
| 23 | C3 | P1 | Low | Regulated industry compliance — one paragraph |
| 24 | C4 | P1 | High | Benchmarking requires running other frameworks |
| 25 | D2-D8 | P1 | Low-Med | Various structural improvements |
| 26 | E2 | P2 | Low | Test references in type error table |
| 27 | G2-G4 | P2 | Low-Med | Effect masking, staged computation, boundary terms |
| 28 | G7 | P2 | High | Presheaf model — mathematically heavy |
| 29 | H1-H4 | P2 | Medium | Structural expansion of companion note |
| 30 | X1-X3 | Both | Medium | Cross-paper items |