Victor Taelin

Victor Taelin is the founder of Higher Order Company and the author of Kind and the Higher-order Virtual Machine (HVM). His work explores how functional programs can share computation, run across many processors and carry machine-checkable guarantees. With his collaborators, he developed Bend, bringing parallel execution into a high-level language and, in its newer generation, connecting AI-written applications with checked proofs. His projects and technical writing span the runtime machinery and the languages built above it.

Language design meets runtime limits

Victor’s project history traces a succession of language experiments and performance problems. He explored John Lamping’s graph-based evaluation algorithm through Optlam and Absal, investigating how computations could share work rather than repeatedly copy it.

At the Ethereum Foundation, Victor worked on the Mist browser before leading a team developing Formality, a proof language intended to address the risks of buggy smart contracts. Formality’s C runtime disappointed him on performance. Later experiments with smaller node representations, tagged pointers and specialized copying operations produced the first HVM implementation in Rust. He subsequently founded Higher Order Company to develop the technology and support further research.

His WebMonkeys tackles parallel computing from another direction: exposing GPU computation to JavaScript. It provides operations for sending data, launching work and retrieving results, while handling the conversion between numerical data and WebGL’s textures and rendering operations. Programmers can express an array computation without managing those graphics details themselves.

What automatic parallelism can do

HVM changes how programs execute. Its interaction-net representation breaks computation into local graph rewrites, allowing independent pieces of work to proceed concurrently. The original runtime combines a linear core, in which each piece of data occurs in one place, with lazy, incremental copying. This reduces the need for synchronization while allowing programs to reuse values. Copying happens as the copies are consumed, rather than requiring an entire structure to be duplicated upfront.

The HVM1 documentation makes the distinction between parallel execution and algorithm design concrete. Its recursive bubble sort gains nothing from additional cores because the algorithm is inherently sequential. A radix sort based on merging immutable trees exposes independent work: in the repository’s benchmark, eight-thread HVM sorted a large list 2.5 times faster than single-threaded GHC, although GHC performed better on one thread. Automatic parallelism distributes work that the computation already permits; it does not remove dependencies between steps.

HVM’s other defining property is beta-optimality, which can avoid repeated work in certain higher-order computations. One practical example is runtime fusion: composing operations such as map f and map g can avoid constructing the intermediate list. HVM1 describes extending this benefit to compositions whose functions are unknown at compile time.

Victor also documents where the promise breaks down. HVM1 is a prototype, does not generally outperform C or Rust, and does not support every lambda-calculus term with the same semantics. Its FAQ acknowledges a surprising case in which HVM takes quadratic time for a function GHC computes in linear time. Proposed remedies involve tradeoffs: adding shared references could reduce copying costs, for example, but would require care to preserve the parallel execution model. These qualifications give “optimal” a specific technical meaning rather than making it a claim of universal speed.

The team’s HVM2 provided a low-level interaction-net representation with compilation to C and CUDA. Bend’s original generation supplied a more approachable language above it, including closures, recursion and familiar high-level syntax. Its summation example illustrates the programmer’s remaining responsibility: splitting a range into independently computed halves exposes parallel work, while adding numbers through one long chain leaves each step waiting for the previous result.

Searching programs and checking their properties

Victor’s work on proof languages and program search explores different ways to make software construction more precise:

• Small proof checkers. Kind, whose implementation was rewritten from JavaScript into Haskell, continues his interest in languages that can check mathematical guarantees about programs. Alongside Formality, it gives proof checking a place in his work beyond runtime performance.
• Shared computation during search. In his add-carry experiment, Victor supplies a binary-addition template with 16 missing bits, yielding 65,536 possible completions. HVM’s superpositions represent alternatives together so related candidates can share computation while being tested. The supplied template constrains the search; the experiment demonstrates reduced repetition within that search, while Victor acknowledges that the general problem remains exponential.
• Checked requirements for AI-written code. Bend’s newer generation combines dependent types, parallel execution and application laws. Developers state required properties in LAWS.bend, and implementations must have proofs checked through PROOF.bend. The intended division of labor leaves people specifying the properties and AI constructing code and proofs that satisfy them.

The Bend game demonstration illustrates that last idea with a formal rule: no sequence of moves may reach victory. An AI can change the board’s behavior, but must also supply a proof that the rule still holds. The guarantee concerns the specified property, so choosing the law remains consequential. Bend also documents limitations in value sharing, proof support and parallel execution. The application language extends Victor’s earlier work into a concrete question: which requirements can people state precisely enough that generated code must demonstrate it preserves them?