HVM and Interaction Calculus: a reliable foundation for AI code

What Victor Taelin is building

To me, the main point of HVM is not another unusual programming language. It is an attempt to give generated code a small, rigorous computational foundation. The HVM2 paper describes the system as a parallel evaluator for extended interaction combinators, with execution on CPUs and CUDA/GPU hardware.

As of the discussion in September 2026, I have not tested this stack in practice, so I will not pretend to have a final verdict. Still, I have followed Victor Taelin's work for a long time: this looks like a consistent engineering direction rather than a sudden project assembled around a fashionable term.

At its core is Interaction Calculus, a compact term language with a spirit close to lambda calculus. Computation is expressed through a small set of nodes and local interaction rules, opening a path to parallel graph reduction.

The HVM2 paper claims near-ideal scaling as cores are added for programs without sequential bottlenecks. A separate CUDA implementation, described in work on a lock-free evaluator, reduced large graphs on GPUs with thousands of concurrent threads. These are author claims and published results, not my own measurements.

HVM4 materials describe the next step: compiling Interaction Calculus functions, including superpositions, directly to machine code without overhead. If this approach remains robust on real programs, the intermediate model stops being elegant theory and becomes a full runtime.

The comparison with Lean is useful only as a rough analogy. The goal is not to ask a model to avoid mistakes, but to constrain its output through a formal system whose execution follows precise rules. HVM, however, is designed primarily for computing code rather than proving mathematical statements.

Why this is more interesting than ordinary prompting

A strict runtime may improve the reliability of AI coding more than another instruction in a system prompt. A model can still generate an incorrect program, but between generation and execution there is now a compact layer with unambiguous semantics.

The practical gain could appear in several places at once: verifiable lowering of code into a small core, explicit handling of duplication and superpositions, and parallel execution that is not limited to CPUs. This is especially interesting for agents that must not merely write program text, but execute and transform it safely.

Where I expect difficulties is in compiling ordinary code into this model conveniently, debugging it, predicting resource use, and closing the gap between impressive parallel demonstrations and everyday sequential tasks. HVM does not look like a replacement for a model's common sense; it looks like a way to make its errors more local and observable. The fate of the idea will be decided in the transition from beautiful reduction to mundane operation.

We previously examined the Claude compiler: what it can build and where its approach breaks down in systems programming. That analysis provides useful context for the Lean compiler idea, where correctness is built through code and formal verification.