Problem: Library summarization is an effective way to accelerate the analysis of client code. However, information about the client is unknown at the time of library summarization, preventing complete summarization of the library. A state-of-the-art approach is Conditional Dyck-CFL Reachability Analysis (ConCRA), which targets graph-reachability-like static analyses and uses hypothetical summaries.

Proposal: Lal et al.⁷ proposed a tensor-product principle: Tensor products with an appropriate detensor operation allow computations to be rearranged in certain ways; for example, they can be used to delay a multiplication in a chain of multiplications. This principle may allow us to generalize, in the summarization framework, Dyck-CFL-reachability-based analyses to algebraic semiring-based analysis.

Follow-up: The library summarization problem can be generalized to partially solving an equation system for a static analysis. Any thoughts on partial evaluation?

Problem: Esparza et al.⁵ generalized Newton’s method to a method for finding fixed points of systems of equations over semirings, leading to a new algorithm to solve interprocedural dataflow analysis. Reps et al.⁸ developed NPA-TP, which extended Esparza’s framework with an improved algorithm for solving linear-context-free-language (LCFL) sub-problems. However, NPA-TP assumes the underlying abstract domain admits an idempotent semiring; such an assumption rules out interesting analysis domains, especially for numerical properties, e.g., the reaching probability.

Proposal: Esparza’s original framework does support non-idempotent semirings, so it would be a good starting point. The NPA-TP framework features tensor products to solve LCFL sub-problems, and from the perspective of algebras, the principle of tensor products does not require idempotence.

Follow-up: Some recent work shows that quantum computation also needs non-idempotent semirings. Can the idea of NPA-TP be generalized to analyze quantum programs?

Problem: In many programs, the manipulation of probability is very complicated and even manual analysis of their correctness is difficult. Consider the problem below:

x = p;
while (prob(0.5)) {
  x = 2 * x;
  if (x >= 1) {
    x = x - 1;
  }
}

We want to verify that at the end of the loop, the probability of the event is exactly .

Proposal: Probability-generating functions provide a succinct way to describe probability distributions of discrete random variables. We might try to derive the probability-generating function of a probabilistic program to reason about the resulting distribution of the program. A recent paper⁹ is in this direction.

Follow-up: There is a connection between derivatives of the probability-generating function of a random variable and the moments of . Can we use the fact to perform moment analysis?

Problem: Static analysis of heap-manipulation programs often involves heap sensitivity. In the simplest case, all memory allocations with the same program location are treated as a single allocation (thus in a context-insensitive way). Advanced techniques include three-valued logic for shape analysis, -CFA, -CFA¹⁰, etc. However, they seem insufficient when we want to analyze recursive programs. (Imagine that in functional programming, iterating over a list is usually implemented as a recursive function.)

Proposal: We can treat the set of all call-strings as a language, then different strategies for handling sensitivity are essentially different ways of defining equivalence classes on the language. A presumably good proposal is to use regular patterns to classify equivalence classes. For example, indicates calling a function an even number of times, an odd number.

Follow-up: In fact, this approach should generalize to all sensitivities that use call strings. Is it meaningful to develop a general framework with regular-pattern-sensitivity?

Problem: Static analysis has long been used to aid formal program verification. What about the reverse: allowing users to supply proofs to aid program analysis? Frama-C already allows users to steer the analysis through directives such as widening hints. Could we go further by letting users inspect an abstract state and prove theorems that justify transforming it in the current program context (e.g., before analyzing the next statement)?

Proposal: This could refine the symbolic abstraction approach¹¹ by allowing users to supply proofs for particular statements. The analyzer might perform symbolic execution to expose a sufficiently precise state for users to reason about.

Follow-up: In what situations would these proofs meaningfully improve the analysis?

Problem: Nondeterminism-first means that we resolve nondeterminism prior to program inputs when defining denotational semantics. For example, suppose that a deterministic function has the signature , then a standard resolution of nondeterminism gives us , but nondeterminism-first suggests . Nondeterminism-first can be useful for e.g., compile-time nondeterminism. A recent study proposed a denotational semantics for probabilistic programs that combines discrete distributions (on a countable state space) and nondeterminism-first. However, it remains open if the semantics can be extended to support continuous distributions.

Proposal: In fact, I do not have any ideas yet.

Follow-up: What about a computational theory for such a combination?

Problem: The common treatment of a probabilistic flip in the semantics is to “split” the current program configuration into two, one for the “world” where the flip shows heads and the other for tails. When we need to deal with multiple concurrent processes, such a treatment means a local flip in a process results in duplicating all other processes. Such a non-local (thus non-compositional) behavior has been shown to be problematic for proving soundness of formal methods (e.g., type systems, which are usually compositional).

Proposal: The result of a probabilistic flip should remain as local as possible. We have recently developed an operational semantics with the desirable locality, but I feel that a more algebraic representation is better. For example, we might want to rearrange the operational semantics to reduction rules and congruence rules. Furthermore, we should prove an equivalence result to the ordinary probabilistic semantics (e.g., Markov chains).

Follow-up: I can always imagine that adding nondeterminism causes a lot of trouble.

Problem: Nondeterminism is often referred to as the basis of abstraction and refinement in the setting of stepwise development¹². However, such a pattern has not been popular in modern programming languages. What is the main obstacle for developing such a framework? Also, people have developed many kinds of semantics for nondeterminism. Which semantics should be the most suitable one for refinement-based programming and reasoning?

Proposal: I guess this has something to do with relational Hoare Logics¹³. At least they provide a way to use nondeterminism in a formal framework of proving program properties.

Follow-up: How to devise a language design for it?

Problem: TileLang and cuTile reflect growing interest in tile-based programming for GPUs, NPUs, and other accelerators. Tile IR is a recent proposal whose semantics is described largely informally. A formal semantics for tile-based programming could provide a foundation for compiling, optimizing, transforming, analyzing, and verifying tile programs.

Proposal: I do not yet have a concrete approach. The first question is where to place the abstraction boundary: which hardware properties should the semantics expose, and which should it abstract away?

Follow-up: Could we define this semantics in the K framework?

Problem: Suppose we have a typed programming language that is suitable for developing embedded Domain Specific Languages (eDSLs). Every eDSL can directly use the base type system from the host language, but it can also have its own advanced domain-specific type system. Languages such as MetaOCaml have already supported such a mechanism, but the interaction between the host language and the eDSL, or maybe even between different eDSLs, is not very convenient yet. It would be nice to have a simple and safe interaction scheme among eDSLs on the same host language.

Proposal: In fact, I do not have any ideas yet.

Follow-up: What else should we have for such a flexible eDSL framework? For example, we might want to consider multi-stage compilation, debuggers, mixed paradigms, etc.

Problem: Array programming (or tensor programming) is pervasive nowadays because of machine learning. Many machine-learning frameworks lack the ability to statically check that tensor shapes are always consistent during program execution. Approaches based on dependent/refinement/indexed types all seem too heavy to become practical.

Proposal: In many (really?) cases, when the input of an array program is fixed, the shapes of all intermediate arrays are also fixed. So we can perform a static shape check after the input is given, but before we execute the program, by propagating the concrete shape information from the given input.

Follow-up: Is it possible to automatically learn the shape-related effects of library functions (e.g., broadcast_tensor)?

Problem: Recently, people have developed verification systems, e.g., CN¹⁴ and RefinedC¹⁵, which integrate refinement types and separation logic to reason about low-level programs. In those systems, refinements seem to still encode purely functional properties (really?). How about enabling type refinements to be separation-logic propositions? To that end, such refined types are not structural any more and we need to work with substructural refinement types. Does the integration make sense?

Proposal: It seems that we can start from linear refinement types.

Follow-up: Linear typing and separation logic share a lot of similarities. Are both rooted in linear logic? If not, what is the fundamental difference?

Problem: Dijkstra monads¹⁶ were originally proposed to automate the verification-condition-generation (VCG) routine for analyzing effectful higher-order programs. They later formed the basis of F*, a proof-oriented programming language¹⁷. One feature of F* is that it supports proof-irrelevant refinement types. Liquid types¹⁸ provide another method of balancing between automatic type inference and dependent typing. One main idea of liquid types is to separately design a language for specification. Can we combine Dijkstra monads and liquid types? What are the benefits—if any—of doing this?

Proposal: So the system is basically a combination of liquid-style language design and F*-style type inference.

Follow-up: Dijkstra monads support multi-monadic effects in a systematic way. This means we might have a method to extend our ICFP paper to include the value interpretation as in the language itself.

Problem: Most current resource-analysis techniques derive linear, polynomial, or exponential bounds. However, when analyzing probabilistic programs, we often encounter bounds that involve fractions. For example, the simple loop while (prob(p)) tick(1); has an expected cost of , where is a program variable that denotes a non-trivial probability.

Proposal: In many cases, a fraction bound can be expressed as a polynomial over another polynomial. So it should be possible to extend current template-based resource-analysis techniques (e.g., AARA) that derive polynomial bounds, by using a template for the denominator to reduce fraction-bound inference to polynomial-bound inference.

Follow-up: A random thought: how can we apply such a resource-analysis technique to Bayesian inference (like a recent paper by Beutner et al.¹⁹)?

Problem: Our ICFP paper presents an extension of AARA that infers upper bounds on the expected cost of probabilistic functional programs with monotone resources (such as time). In general, combining probability and non-monotone resources (such as memory) is unreasonably complex²⁰. Applying optional stopping theorems, people have successfully developed techniques for analyzing arithmetic programs. It would be interesting to see if the whole methodology applies to functional programming, where we have inductive data structures (that can hold potential) instead of numbers.

Proposal: One version of optional stopping theorems states that the expected change in one evaluation step should be “bounded.” This should intuitively hold for functional programming (I mean, in most cases) because one step should change the size of a data structure by at most one (consider the case of cons). By constructing a suitable Markov chain, we might be able to reason about probabilistic functional programs with non-monotone resources.

Follow-up: Optional stopping theorems always talk about “expected change” and “expected termination time.” Why them?!

Problem: Apply the Newtonian Program Analysis (NPA) framework⁵ and its extension⁸ to carry out resource analysis. Existing work has shown the possibility to perform recurrence-based analysis²¹. How about other kinds of resource analysis, like AARA?

Proposal: Because amortized analysis is naturally two-vocabulary, it seems possible to recast AARA as a two-vocabulary abstract domain. The gap is that AARA is constraint-based, which differs from the general NPA framework.

Follow-up: NPA basically provides a framework for analyzing non-linear-recursive programs by iteratively analyzing linear-recursive programs. Can we combine this idea to iteratively use AARA to solve linear recursion?

Problem: Most work on resource analysis focuses on worst-case upper bounds, but in practice people also want to know worst-case lower bounds, i.e., whether there exists a realizable execution path leading to the bound. This could usually be done by testing techniques for worst-case analysis, e.g., fuzzing²². Recent advances in incorrectness logic²³ and coverage typing²⁴ show the power of such realizability analysis. We want to follow those lines of work to build type systems or program logics to reason about worst-case lower bounds.

Proposal: From the perspective of incorrectness logic, one can extend separation logic with time credits. From the perspective of coverage typing, one can extend liquid resource types.

Follow-up: Is it possible to integrate such deductive analysis with fuzzing-based worst-case analysis?

Problem: AARA is a mathematically elegant approach, but it is still far from analyzing real-world programs to identify performance bottlenecks. With the evolution of LLMs, it seems promising to apply them in real-world program analysis. An interesting approach is HoarePrompt²⁵, which drives the LLM to perform Hoare-style strongest postcondition reasoning to detect bugs. I wonder if this approach could generalize to resource analysis, in the sense that the LLM uses its reasoning capability to analyze the potential functions in natural language.

Proposal: Maybe go from Hoare logic to quantitative Hoare logic²⁶? Or for performance bottleneck analysis, incorrectness-logic-style approaches could be better, e.g., our ESOP paper.

Follow-up: There is some possibility to develop a finer-grained integration. Hybrid Resource Analysis^{27 28} presents a theoretical framework to integrate different resource analyses in AARA, so, for example, it is interesting to see if one can use an LLM to analyze unsafe Rust code, derive the boundary information, and then integrate it back into an AARA analysis to analyze safe Rust code.

Problem: Pattern fuzzing offers an approach to worst-case analysis that searches a space of test-input generators (i.e., patterns)²². This avoids directly fuzzing inputs, which can be very large in performance testing, and produces generators capable of producing arbitrarily large test cases. One limitation is that users have to adapt the patterns when moving to a different system under test (SUT). The success of LLMs in software engineering suggests a possibility: could an agent discover and fuzz these patterns?

Proposal: There are two possible approaches. The agent could generate and modify generator programs directly, or it could design a pattern DSL and use conventional pattern fuzzing to search within that DSL. The latter might reduce token usage.

Follow-up: Can we meaningfully integrate this approach with AARA-style reasoning?

Problem: Semantic-type-guided bug finding²⁹ reformulates symbolic execution in terms of incorrectness reasoning. Symbolic execution has also been used to find performance bugs through worst-case analysis³⁰. Given the semantic typing approach to AARA³¹, a natural question is whether semantic-type-guided bug finding can be extended to detect excessive resource usage or other performance bugs.

Proposal: I do not yet have a concrete approach. Could the existing semantic typing account of AARA make this extension straightforward?

Follow-up: Could this also help detect non-termination bugs?

Problem: Daniel Ritchie suggested generative probabilistic programming for procedural modeling and design (the use of random programs to generate visual content with respect to aesthetic or functional constraints). Such an approach has been rediscovered in several individual developments, such as Scenic³² and Picture³³. So instead of separate developments, we want to develop a framework to ease such domain-specific procedural design.

Proposal: This has something to do with the eDSL framework.

Follow-up: It might be interesting to see how such static procedural design evolves to dynamic procedural design (e.g., synthesis of an environment). Another direction is interactive refinement (e.g., incorporating feedback from users) of the generated designs.

Problem: A recent paper by Cusumano-Towner et al.³⁴ studies how to ease the burden of implementing involutive MCMC by combining probabilistic programming and differentiable programming. It still remains a challenge (um, you have to double-check) to statically verify the correctness of a concrete implementation in their framework.

Proposal: I would try to combine type systems for sound programmable inference and sound differentiable programming.

Follow-up: I am thinking of The Next XXX MCMC Algorithms.

Problem: Quantum physics uses a form of complex probability. People have been thinking of it as a serious probability theory (see this and this). There are even quantum analogs of Bayesian inference (one and the other). Does it make sense to incorporate some of those ideas in current probabilistic programming systems?

Proposal: I still have to learn quantum physics (um, not really).

Follow-up: Some people are trying to add quantum features to standard Bayesian models (check out this).

Problem: At the time of writing this page, system-one models (like Jev and Laya) are under active discussion. These models have the instruction understanding capability of LLMs, but they are designed to make probabilistic decisions from a given answer space, i.e., the support of a probability distribution. Such models may be more suitable to integrate with probabilistic programming than generative LLMs (e.g., as done in LLaMPPL³⁵), especially in the programmable inference setting, where the system-one models could either provide model or guide samples.

Proposal: Currently, system-one models support discrete distributions with a finite support. So, they might be suitable for Bayesian inference with discrete latent variables.

Follow-up: How to extend from discrete distributions to continuous distributions?

Problem: There exists work that models PBT as probabilistic programming³⁶, in the sense that one first implements a generator with tunable parameters, and then carries out optimization towards a target distribution (or to maximize metrics such as entropy). However, PBT usually consists of two components: one is input generator, and the other is test reducer. The latter is called delta debugging in some other context; some recent work studies how to reduce tests while preserving validity³⁷, where the idea is to reduce in the space of generator traces, rather than inputs themselves. It becomes natural to ask if one could establish a comprehensive probabilistic programming framework for both the generation and the reduction.

Proposal: The validity-preserving delta debugging work reminds me of trace-based probabilistic programming. The test reduction then operates on the traces, with the intuition that the simulation of the new traces still yields valid test inputs. Trace types and our papers on guide types (PLDI and OOPSLA) provide static methods to reason about the structural shape of traces. So a trace-based PBT could be built upon a programmable inference core: perform inference or optimization on the trace space for tuning generators, transform traces while preserving types for reducing inputs, and both phases could be user-programmable to improve performance.

Follow-up: Semantic validity is still hard; adding refinement types could help, but it may be too heavy. Maybe involutive could help here.

Problem: One central function of low-code programming platforms is to automatically generate a usable interface for manipulating database tables. In an application, the developers might want to customize a specific way to organize the interface, and they want to reuse the customization across the application.

Proposal: The customization can be thought of as a functor that takes a database-table module as its input and outputs an interface module for that table. For low-code programming, it would be useful to have a mechanism where the developers customize a table interactively and the platform automatically synthesizes the code of the customization functor.

Follow-up: Low-code programming involves many UI-related customizations. Is there a more general principle? For example, it might be interesting to investigate Natural Programming.

Problem: Recently, resource-guided synthesis and algorithm synthesis have received considerable attention^{38 39}. We have also published a related PLDI paper. Those approaches can be categorized into two sorts: one develops a complex type system or program logic to enforce resource guarantees; the other proposes algorithmic templates that ensure resource guarantees. The latter is somewhat related to Implicit Computational Complexity (ICC), which characterizes algorithms by constraints on the way in which they are constructed. In other words, ICC research usually provides a non-standard programming language, in which every legal program is guaranteed to have a certain complexity. Can we generalize the template-based approach to an ICC-based approach?

Proposal: A starting point could be non-size-increasing computation⁴⁰.

Follow-up: ICC seems to be not so fine-grained, e.g., usually researchers focus on whether the complexity is polynomial or not. How to make them finer-grained? For example, would it be possible to develop an ICC class for algorithms?

Problem: Verified Software Toolchain (VST) is a set of verified tools that formally verify the functional correctness of C programs using Hoare logic and separation logic. I wonder if it is also convenient to verify resource-usage properties of C programs, like their time or memory complexities.

Proposal: It has been shown that separation logic naturally supports resource verification based on time credits⁴¹. So conceptually it should be possible to have that in VST.

Follow-up: Can we develop some general reasoning libraries for resource verification?

Problem: Many verification projects (e.g., seL4) start from a high-level specification implemented in a functional language (e.g., Haskell) and then prove that a concrete implementation in a system programming language (e.g., C) refines the specification. From the perspective of software engineering, this suggests another way of system programming: first implement a functional specification and then (iteratively) refine it to build a concrete low-level implementation.

Proposal: Build a language where the high-level and low-level languages can interoperate seamlessly, e.g., Haskell and C. Existing solutions are somehow quite complex, in the sense that they want to interoperate with a realistic C compiler directly. However, it would be nice enough for the development process if the C part is just supported partially, but with better support, e.g., to be equipped with an interpreter.

Follow-up: What is the best practice for multi-language (i.e., multilingual) software engineering?

Problem: In theorem provers, existential variables (or evars) are placeholders for unknown values that the prover can instantiate later in a proof. A similar mechanism could be useful in symbolic-execution-based program verifiers such as VeriFast. When applying a lemma or transforming a predicate, users could leave some values unspecified and let the symbolic executor determine them later.

Proposal: A starting point is to adapt the mechanism used in theorem provers: record assignable metavariables and instantiate them through unification. The main question is when to perform unification. For example, unfolding an array predicate could introduce an evar for the element being accessed; symbolic execution of a later array access could then instantiate it. This suggests a connection to biabduction-style reasoning.

Follow-up: Could evars support customizable strategies for automated symbolic verification, similar to user-defined tactics in Rocq?

Problem: Finally tagless interpretation is a functional programming technique for embedding DSLs in a host language through functions or type classes. For verification-oriented symbolic execution, avoiding a deep embedding or an intermediate representation could improve diagnostics, help address the expression problem, and perhaps improve performance.

Proposal: The symbolic execution signature could operate on partial statements that form a flattened decomposition of a program. The intended scope is imperative programs with structured control flow (break and continue are allowed, but goto is not). A finally tagless executor could allow a program to be developed and verified at the same time. With an LCF-style theorem prover, we could extend the signature with operations for supplying specifications and invariants and proving that one symbolic state entails another.

Follow-up: Could we reverse the embedding: keep the DSL as a standalone language and embed host-language code in comments or special attributes? What if the host language and the DSL were then the same language? This could be an interesting interface for program verification.

Problem: Property-based testing (PBT) uses randomly generated inputs to check selected properties of a system under test. These properties are often easier to specify than full functional correctness. A similar perspective could be useful in formal program verification: a complete specification may be difficult or even impractical to write, or we may only need to establish a few key properties. Could we support this style of verification while reusing proofs across properties?

Proposal: Proof reuse is the main challenge. Characteristic formulae⁴² may offer a starting point. The conjunction rule of Hoare logic is another possibility, though combining it with separation logic is not straightforward.

Follow-up: Could intersection types connect this approach with input-output examples and counterexamples?

Problem: Prophecy variables have been used to verify functional properties of Rust programs with unsafe code in Iris; see RustHornBelt⁴³. Our OOPSLA paper introduces prophecy potential for AARA-style resource analysis. Could we develop a notion of prophecy resource in Iris and extend semantic typing to support it for Rust program verification?

Proposal: The difficult part is borrowing. A prophecy variable provides a pure fact equating its value with the value held by the borrowed location when the borrow ends. Resources, however, are not pure facts. Would prophecy resources require an explicit account of the exclusivity of mutable access, perhaps by extending the lifetime logic to model Stacked Borrows?

Follow-up: Extending RustBelt’s adequacy theorem to Stacked Borrows is another interesting direction.

Problem: Forward symbolic execution based on strongest postconditions is a key component of formal program verification. Implementing it through tactics in a theorem prover can be slow, while a direct implementation may contain soundness bugs. Inspired by Milawa⁴⁴, could we build a symbolic executor in stages, incrementally obtaining an efficient, certified implementation?

Proposal: To support self-certification, we could start with a verification-oriented language such as C*, perhaps reduced to a small core.

Follow-up: Once the methodology is clear, could an agent carry out the construction?

Problem: Two established approaches to shape analysis use separation logic (e.g., through biabduction) and three-valued logic⁴⁵. How do these approaches compare, and could combining their ideas lead to a useful variant of separation logic?

Proposal: The goal is to improve automation for separation-logic-based reasoning. I do not yet have a concrete approach.

Follow-up: Can we establish a formal connection between the two approaches to shape analysis?

Problem: Although LLMs have become really powerful in theorem proving, specification engineering is still a bottleneck for certified software engineering. Writing a spec, or generating a spec for natural-language requirement, are still cumbersome or not trustworthy. Even worse, it is from time to time unclear what the functional spec is, especially during the active development of software. On the other hand, there are many desirable, relatively well-defined, high-level specifications, such as memory safety, datarace free, deadlock free, termination, refinement w.r.t. another existing program or model, etc. I want to develop a framework, such that one can easily develop and combine different high-level specifications, and the framework yields a symbolic executor for the combined spec, possibly in a C* style of allowing manual proof blocks.

Proposal: Inspired by Iris’s resource, each high-level specification could be treated as a ghost state (or invariant). Different specs can be combined as a product of different ghost states (like an extensible row). When developing, one needs to define the symbolic-execution rules under a particular ghost resource. Each spec may also supply some ghost commands that can be used in proof blocks. For example, refinement-based specs can be modeled by a recently proposed embedding of relational Hoare logic into a standard one⁴⁶.

Follow-up: There are Program Logics à la Carte⁴⁷ and Meta-theory à la carte⁴⁸.

Problem: Rocq proofs are organized in a forward, tactic-based manner, which is not very readable. In contrast, Isabelle (and some other theorem provers) provides a backward mode, where the intermediate goals are stated explicitly, which improves readability. Is it possible to use a backward pattern in Rocq proofs? If not, would it be possible to have a backward-proof DSL that can be translated to Rocq?

Proposal: Isabelle’s Isar might be a good starting point.

Follow-up: What is the best proof interface for system programmers?

Problem: In separation logic, we define memory predicates to describe data structure layouts. Reasoning about traversal often requires additional predicates, such as lseg for sll and a zipper for a tree. Inspired by Church encodings, could we instead define memory predicates through their elimination forms, specifying how they can be used? This would require reasoning about magic wands, which may complicate automation. With LLMs assisting in proof construction, however, such explicit interfaces could be useful for agentic program verification.

Proposal: For example, the array predicate char_array a n cs could be defined recursively by forall i. [0 <= i < n] -* (a + i) |-> cs[i] ** (forall v. (a + i) |-> v -* char_array a n cs{i |-> v}). The immediate question is how to justify this definition: it is recursive but not an ordinary inductive definition.

Follow-up: Could HOL’s new-specification mechanism help? We would first need to prove that a predicate char_array satisfying this property exists.

Problem: A recent POPL paper⁴⁹ uses algebraic structures to automate separation logic proofs. The approach does not seem to handle memory predicates well, especially those defined inductively over complex data structures. Many such predicates, including sll, lseg, and treerep, can be viewed as folds over logical objects. Could the equational theory of catamorphisms help automate proofs about these predicates?

Proposal: Related program synthesis approaches^{50 51} suggest a possible direction: use the algebraic structure to generate propositions that are easier to prove or manipulate.

Follow-up: Extending this approach from catamorphisms to paramorphisms seems like a natural next step.

Problem: As LLMs generate larger proofs, theorem prover runtime and memory usage can become bottlenecks in large-scale proving and verification. The computational structure of LCF-style HOL provers may make them a more tractable optimization target than provers based on dependent types; this blog post offers a related perspective. One concrete question is whether memory allocation can be tailored to LCF-style proving: types, terms, and theorems are usually small objects, and proof construction creates large numbers of them.

Proposal: Generational garbage collection may be a good fit. Functional in-place programming is also worth exploring⁵².

Follow-up: Could we view the HOL kernel interface as a control plane and ask an agent to generate certified fast paths for recurring proof operations? Normalization by evaluation in an LCF system⁵³ offers one example.

Problem: I had an LMPL paper about applying algebraic effects to engineer LLM-integrated scripts. (There is a parallel LMPL paper in the same direction: Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad.) Since then, LLM engineering practice has shifted from workflows to agents, and to harnesses. Some people also call harnesses “AgentOS”, operating systems designed around LLMs. The idea is rather simple: algebraic effects provide a clean way to separate semantics from syntax, achieving good abstraction for building effectful software; on the other hand, LLM-integrated scripts need to handle many different kinds of effects, e.g., remote calls, bash executions, async schedules, multi-agent coordination, branch selections, and so on. DeepSeek Harness also employs an effect-and-coeffect plugin system, aiming at modularity and extensibility. Currently, the popular languages for implementing harnesses are Python and TypeScript, which lack good support for algebraic effects, from the perspective of either the runtime or the type system.

Proposal: Design a new programming language with the following features: (i) multi-shot effect handlers with a high-performance runtime (e.g., as a sandbox), (ii) support for hot code updates (like Erlang), so as to support dynamic plugin management, (iii) a type system to track resources, capabilities, and effects.

Follow-up: It is also interesting to see if choreographic programming can be applied here, in the sense of multi-agent systems or even distributed-agent systems.

Problem: In the current LLM workflows, tool calls are essential to grant agents powerful capabilities to do many kinds of work. Interestingly, from the perspective of LLM calls, tool calls are fully syntactic: an LLM request only carries the description and schema for each available tool. However, current agents/harnesses usually couple tools with their concrete implementations. Some frameworks may support tool customization, but the semantics is still tightly coupled.

Proposal: Suppose we have a harness that treats tools as effectful operations without semantics. Their semantics should be determined dynamically by effect handlers. So the harness should be able to write code to implement handlers, as well as push handlers onto and pop handlers off the runtime effect stack. This seems an interesting generalization of the code-action paradigm.

Follow-up: This seems quite interesting and powerful, but is it really useful?