Contents

1 Introduction

Nock is a combinator calculus which serves as the computational specification layer for the Urbit and Nockchain/NockApp systems. It is a hyper-risc instruction set architecture (ISA) intended for execution by a virtual machine (but see ~mopfel-winrux, pp. 99–130 in this volume). Nock’s simplicity and unity of expression make it amenable to proof-based reasoning and guarantees of correctness. Its Lisp-like nature surfaces the ability to introspect on the code itself, a property which higher-level languages compiling to it can exploit. Yet for all this, Nock was not born from a purely mathematical approach, but found its roots in practical systems engineering.

Nock permits itself a finite number of specification changes, called “decrements” or “kelvins”, which allow it to converge on a balance of expressiveness and efficacy. This article outlines the extant historical versions of the Nock combinator calculus and reconstructs the motivation for the changes made at each kelvin decrement. It begins with an exposition of Nock as a tool of computation, outlines the history of Nock’s decrements, and speculates on motivations for possible future developments.

2 Nock as a Combinator Calculus

Fundamental computer science research has identified a family of universal computers which may be instantiated in a variety of ways, such as the Turing machine, the lambda calculus, and the combinator calculus. Equivalence theorems such as the Church–Turing thesis show that these systems are equivalent in their computational power, and that they can be used to compute any computable function. The combinator calculus is a family of systems which use a small set of combinators to express computation. The most well-known member of this family is the ski combinator calculus, which uses only three combinators: s, k, and i. Other members of this family include the bckw combinator calculus and the h combinator calculus. These systems are all equivalent in their computational power, but they differ in their syntax and semantics. The Nock combinator calculus is an extension of the ski combinator calculus which adds a few axiomatic rules to navigate and manipulate binary trees, carry out a very primitive arithmetic, and provide for side effects.

Put perhaps better, Nock is a family of combinator calculi that sequentially converge on an “optimal” expressiveness for certain design desiderata. This includes an economy of expression (thus several macro opcodes) and consideration of how a higher-level language would invoke stored procedural expressions. Furthermore an opcode exists which produces and then ignores a computation, intended to signal to a runtime layer that a side effect may be desired by the caller.¹

Nock bears the following characteristics:

• Turing-complete. Put formally, Turing completeness (and thus the ability to evaluate anything we would call a computation) is exemplified by the \(\mu \)-recursive functions. In practice, these amount to operations for constant, increment, variable access, program concatenation, and looping (Reitzig, 2012). Nock supports these directly through its primitive opcodes.

• Functional (as in language). Nock is a pure function of its arguments. In practice, the Urbit operating system provides a simulated global scope for userspace applications, but this virtualized environment reduces to garden-variety Nock. (See ~lacnes, pp. 71–97 in this volume, for details of a Nock virtualized interpreter.)

• Subject-oriented. Nock evaluation consists of a formula as a noun to be evaluated against a subject as a noun. Taken together, these constitute the entire set of inputs to a pure function.

  Some Nock opcodes alter the subject (for instance a variable declaration) by producing a new subject which is utilized for subsequent axis lookups.

• Homoiconic. Nock unifies code and data under a single representation. A Nock atom is a natural number, and a Nock cell is a pair of nouns. Every Nock noun is acyclic, and every Nock expression is a binary tree. For example, Nock expressions intended to be evaluated as code are often pinned as data by the constant opcode until they are retrieved by evaluating the constant opcode at that axis.

• Untyped. Nock is untyped, meaning that it does not impose any type system on the expressions it evaluates. Nock “knows” about the natural numbers in two senses: such are used for addressing axes in the binary tree of a noun, and such are manipulated and compared using the increment and equality opcodes.

• Solid-state. A Nock interpreter is a solid-state machine, meaning that it operates from a state to a new state strictly according to inputs as a pure lifecycle function. The Nock interpreter must commit the results of a successful computation as the new state before subsequent computations, or events, can be evaluated. Transient evaluations (uncompleted events) and crashes (invalid evaluations) may be lost without consequence, and the Nock interpreter layer persists the underlying state of the machine.

We have asserted without demonstration thus far that Nock is a combinator calculus. We now show that this is the case, with reference to Nock 4K, the latest specification. The simplest combinator calculus consists of only three combinators: s, k, and i (Wolfram, 2021). These combinators are:

1.

s substitution. \(\textsc {s}xyz = xz(yz)\), returns the first argument applied to the third, then applies this to the result of the second argument applied to the third. This corresponds to Nock 4K’s opcode 2, which substitutes the second argument into the first argument at the third argument’s axis. (There are some subtle differences to Nock’s expression of s as opcode 2 that we will elide as being fundamentally similar, but perhaps worthy of its own monograph.)

2.

k constant. \(\textsc {k}xy = x\), consumes its argument and returns a constant in all cases. This corresponds to Nock 4K’s opcode 1, which yields its argument as a constant noun.

3.

i identity. \(\textsc {i}x = x\), returns its argument. This corresponds to a special case of Nock 4K’s opcode 0, a generalized axis lookup operator, which can trivially retrieve the current subject or expression as well as any children.

While Nock introduces a few more primitive operations as a practicality, the above identities establish its bona fides as a combinator calculus capable of general computation. Similar to Haskell Curry’s bckw system, which can be written in forms isomorphic to ski, Nock provides a set of primitive rules and a set of economic extended rules for convenience in writing a compiler.²

In an early document, Yarvin explained two of his design criteria in producing Nock as a practical isa target (~sorreg-namtyv, 2010):

1.

Natural conversion of source to code without other inputs.

2.

Metacircularity without deep stacks; i.e., the ability to extend Nock semantics without altering the underlying substrate.

This latter idea he particularly connected to the concept of what came to be called a “scry namespace”: “dereferencing Urbit paths is as natural (and stateless) a function as increment or equals” (ibid.). Indeed, Urbit’s current userspace utilizes such an affordance to replicate a global scope environment for accessing system and remote resources. (See ~lacnes, pp. 71–97 in this volume, for a discussion of the Nock virtualized interpreter.)

3 Nock’s Decrements

The Nock family survives in a trail of breadcrumbs, with each version of the specification being a decrement of the previous version.³ Early versions were produced exclusively by Curtis Yarvin, eventually involving the input of other developers after the 2013 founding of Tlon Corporation. In this section, we present each extant version of the Nock specification and comment on the changes and their motivations. Only the layouts have been changed for print. Dates for Nock specifications were derived from dated public posts (U, 9K), internal dating (13K, 12K, 11K, 10K), or from Git commit history data (8K, 7K, 6K, 5K).⁴ No version of 14K survives publicly, nor does any primordial version prior to U (15K) appear to exist.

Yarvin’s background as a systems engineer with systems like Xaos Tools (for sgi Irix), Geoworks (on DoCoMo’s iMode), and Unwired Planet (on the Wireless Application Protocol, wap) inclined him towards a formal break with Unix-era computing (~sorreg-namtyv, 2025). He sought to produce a system enabling server-like behavior rather than a network of clients dependent on centralized servers for a functional Internet. This required a deep first-principles rederivation of computing; the foundational layer was a combinator calculus which became Nock. Nock was intended from the beginning to become less provisional over time, encoding a kelvin decrement which forced the specification to converge on a sufficiently good set of opcodes. Many downstream consequences of Urbit and NockApp as systems derive directly from the affordances encoded into Nock.

3.1 U

I have not really worked with combinator models, but my general impression is that it takes essentially an infinite amount of syntactic sugar to turn them into a programming language. U certainly takes some sweetener, but not, I think, as much. (~sorreg-namtyv⁵ , 2006)

The earliest extant Nock is U, a proto-Nock posted to the Lambda the Ultimate blog in 2006 (~sorreg-namtyv (2006); ~sorreg-namtyv (2006)).⁶ The draft is versioned 0.15; subsequent evidence indicates that this is a downward-counting kelvin-versioned document already. The full specification is reproduced in Listing 1.

Extensive commentary on the operators is provided. Rightwards grouping of tuple expressions has already been introduced. Extension of the language is summarily ruled out.⁷ Data are conceived of as Unix-like byte streams; details of parsing and lexing are considered. Terms (the ancestor of nouns) include a NULL-like “foo” type ~ distinguishable by value rather than structure. ascii is built in as numeric codes, evocative of Gödel numbering.

As commenter Mario B. pointed out, the U specification permits ski operators with the simple expressions,

   [name]   [pattern]            [definition] 
    (I)      (I $a)               $a 
    (K)      (K $a $b)            $b 
    (S)      (S $a $b $c)         ($a $c ($b $c))

While early work (1940s–50s) had been carried out on “minimal instruction set computers” (miscs), it is more likely that Yarvin was influenced by contemporaneous work on “reduced instruction set computers” (riscs) in the 1980s and 90s. Language proposals like that of Madore’s Unlambda and Burger’s Pico Lisp may have influenced Yarvin’s design choices throughout this era.

The U specification is in some ways the single most interesting historical document of our series. Yarvin particularly identified a desire to avoid baking abstractions like variables and functions into the U cake, and an emphasis on client–server semantics. The scry namespace appears for the first time as a referentially transparent immutable distributed namespace. U expresses a very ambitious hyper-Turing operator, acknowledging that its own instantiation from the specification is impossible and approximate. Yarvin grapples in U with the halting problem (via his follow operator) and with the tension between a specification and an implementation (a gulf he highlighted as a human problem in his 2025 LambdaConf keynote address). Furthermore, asides on issues like the memory arena prefigure implementation details of Vere as a runtime.

U: Definition 
 
1 Purpose 
    This document defines the U function and its data 
5    model. 
 
2 License 
    U is in the public domain. 
 
103 Status 
    This text is a DRAFT (version 0.15). 
 
4 Data 
    A value in U is called a "term."  There are three 
15    kinds of term: "number," "pair," and "foo." 
 
    A number is any natural number (ie, nonnegative 
    integer). 
 
20    A pair is an ordered pair of any two terms. 
 
    There is only one foo. 
 
5 Syntax 
25    U is a computational model, not a programming 
    language. 
 
    But a trivial ASCII syntax for terms is useful. 
 
305.1 Trivial syntax: briefly 
    Numbers are in decimal.  Pairs are in parentheses 
    that nest to the right.  Foo is "~". 
 
    Whitespace is space or newline.  Line comments 
35    use "#". 
 
5.2 Trivial syntax: exactly 
    term    : number 
            | 40 ?white pair ?white 41 
40            | foo 
 
    number  : 48 
            | [49-57] *[48-57] 
 
45    pair    : term white term 
            | term white pair 
 
    foo     : 126 
 
50    white   : *(32 | 10 | (35 *[32-126] 10)) 
 
6 Semantics 
    U is a pure function from term to term. 
 
55    This document completely defines U.  There is no 
    compatible way to extend or revise U. 
 
6.1 Rules 
    [name]   [pattern]                [definition] 
60 
    (a)      ($a 0 $b)                $b 
    (b)      ($a 1 $b $c)             1 
    (c)      ($a 1 $b)                0 
    (d)      ($a 2 0 $b $c)           $b 
65    (e)      ($a 2 %n $b $c)          $c 
    (f)      ($a 3 $b $c)             =($b $c) 
    (g)      ($a 4 %n)                +%n 
 
    (h)      ($a 5 (~ ~ $b) $c)       $b 
70    (i)      ($a 5 (~ $b $c) $d)      *($a $b $c $d) 
    (j)      ($a 5 (~ ~) $b)          ~ 
    (k)      ($a 5 (~ $b) $c)         *($a $b $c) 
    (l)      ($a 5 ($b $c) $d) 
                            (*($a $b $d) *($a $c $d)) 
75    (m)      ($a 5 $b $c)             $b 
 
    (n)      ($a 6 $b $c)   *($a *($a 5 $b $c)) 
    (o)      ($a 7 $b)                *($a 5 $a $a $b) 
    (p)      ($a 8 $b $c $d)          >($b $c $d) 
80 
    (q)      ($a $b $c)     *($a 5 *($a 7 $b) $c) 
    (r)      ($a $b)                  *($a $b) 
    (s)      $a                       *$a 
 
85    The rule notation is a pseudocode, only used in 
    this file. Its definition follows. 
 
6.2 Rule pseudocode: briefly 
    Each line is a pattern match.  "%" means 
90    "number."  Match in order.  See operators below. 
 
6.3 Rule pseudocode: exactly 
    Both pattern and definition use the same 
    evaluation language, an extension of the trivial 
95    syntax. 
 
    An evaluation is a tree in which each node is a 
    term, a term-valued variable, or a unary 
    operation. 
100 
    Variables are symbols marked with a constraint. 
    A variable "$name" matches any term.  "%name" 
    matches any number. 
 
105    There are four unary prefix operators, each of 
    which is a pure function from term to term: "=", 
    "+", "*", and ">". Their semantics follow. 
 
6.4 Evaluation semantics 
110    For any term $term, to compute U($term): 
 
        - find the first pattern, in order, that 
          matches $term. 
        - substitute its variable matches into its 
115          definition. 
        - compute the substituted definition. 
 
    Iff this sequence of steps terminates, U($term) 
    "completes." Otherwise it "chokes." 
120 
    Evaluation is strict: incorrect completion is a 
    bug.  Choking is U's only error or exception 
    mechanism. 
 
1256.5 Simple operators: equal, increment, evaluate 
    =($a $b) is 0 if $a and $b are equal; 1 if they 
    are not. 
 
    +%n is %n plus 1. 
130 
    *$a is U($a). 
 
6.6 The follow operator 
    >($a $b $c) is always 0.  But it does not always 
135    complete. 
 
    We say "$c follows $b in $a" iff, for every $term: 
 
        if *($a 5 $b $term) chokes: 
140            *($a 5 $c $term) chokes. 
 
        if *($a 5 $b $term) completes: 
            either: 
                *($a 5 $c $term) completes, and 
145                *($a 5 $c $term) equals 
                  *($a 5 $b $term) 
            or: 
                *($a 5 $c $term) chokes. 
 
150    If $c follows $b in $a, >($a $b $c) is 0. 
 
    If this statement cannot be shown (ie, if there 
    exists any $term that falsifies it, generates an 
    infinitely recursive series of follow tests, or is 
155    inversely self-dependent, ie, exhibits Russell's 
    paradox), >($a $b $c) chokes. 
 
7 Implementation issues 
    This section is not normative. 
160 
7.1 The follow operator 
    Of course, no algorithm can completely implement 
    the follow operator.  So no program can completely 
    implement U. 
165 
    But this does not stop us from stating the 
    correctness of a partial implementation - for 
    example, one that assumes a hardcoded set of 
    follow cases, and fails when it would otherwise 
170    have to compute a follow case outside this set. 
 
    U calls this a "trust failure."  One way to 
    standardize trust failures would be to standardize 
    a fixed set of follow cases as part of the 
175    definition of U.  However, this is equivalent to standardizing a fixed trusted code base.  The 
    problems with this approach are well-known. 
 
    A better design for U implementations is to 
    depend on a voluntary, unstandardized failure 
180    mechanism.  Because all computers have bounded 
    memory, and it is impractical to standardize a 
    fixed memory size and allocation strategy, every 
    real computing environment has such a mechanism. 
 
185    For example, packet loss in an unreliable packet 
    protocol, such as UDP, is a voluntary failure 
    mechanism. 
 
    If the packet transfer function of a stateful UDP 
190    server is defined in terms of U, failure to 
    compute means dropping a packet.  If the server 
    has no other I/O, its semantics are completely 
    defined by its initial state and packet function. 
 
1957.2 Other unstandardized implementation details 
    A practical implementation of U will detect and 
    log common cases of choking.  It will also need a 
    timeout or some other unspecified mechanism to 
    abort undetected infinite loops. 
200 
    (Although trust failure, allocation failure or 
    timeout, and choke detection all depend on what 
    is presumably a single voluntary failure 
    mechanism, they are orthogonal and should not be 
205    confused.) 
 
    Also, because U is so abstract, differences in 
    implementation strategy can result in performance 
    disparities which are almost arbitrarily extreme. 
210    The difficulty of standardizing performance is 
    well-known. 
 
    No magic bullet can stop these unstandardized 
    issues from becoming practical causes of lock-in 
215    and incompatibility. Systems which depend on U 
    must manage them at every layer.

Source: ~sorreg-namtyv (2006).

3.2 Nock 13K

At some point between January 2006 and March 2008, Nock acquired its cognomen.

The only compound opcode is opcode 6, the conditional branch opcode.

Axiomatic operator * tar⁸ is identified as a GOTO.⁹

Author: Curtis Yarvin (curtis.yarvin@gmail.com) 
Date: 3/8/2008 
Version: 0.13 
 
51. Manifest 
 
    This file defines one Turing-complete function, 
    "nock." 
 
10    nock is in the public domain.  So far as I know, 
    it is neither patentable nor patented.  Use it at 
    your own risk. 
 
2. Data 
15 
    Both the domain and range of nock are "nouns." 
 
    A "noun" is either an "atom" or a "cell."  An 
    "atom" is an unsigned integer of any size.  A 
20    "cell" is an ordered pair of any two nouns, the 
    "head" and "tail." 
 
3. Pseudocode 
 
25    nock is defined in a pattern-matching pseudocode. 
 
    Match precedence is top-down.  Operators are 
    prefix.  Parens denote cells, and group right: 
    (a b c) is (a (b c)). 
30 
4. Definition 
 
4.1 Transformations 
 
35      *(a 0 b c)   => *(*(a b) c) 
      *(a 0 b)     => /(b a) 
      *(a 1 b)     => (b) 
      *(a 2 b)     => **(a b) 
      *(a 3 b)     => &*(a b) 
40      *(a 4 b)     => ^*(a b) 
      *(a 5 b)     => =*(a b) 
      *(a 6 b c d) => *(a 2 (0 1) 
                            2 (1 c d) (1 0) 
                            2 (1 2 3) (1 0) 4 4 b) 
45      *(a b c)     => (*(a b) *(a c)) 
      *(a)         => *(a) 
 
4.2 Operators 
 
504.2.1 Goto (*) 
 
      *(a)             -> nock(a) 
 
4.2.2 Deep (&) 
55 
      &(a b)           -> 0 
      &(a)             -> 1 
 
4.2.3 Bump (^) 
60 
      ^(a b)           -> ^(a b) 
      ^(a)             -> a + 1 
 
4.2.4 Same (=) 
65 
      =(a a)           -> 0 
      =(a b)           -> 1 
      =(a)             -> =(a) 
 
704.2.5 Snip (/) 
 
      /(1 a)           -> a 
      /(2 a b)         -> a 
      /(3 a b)         -> b 
75      /((a + a) b)     -> /(2 /(a b)) 
      /((a + a + 1) b) -> /(3 /(a b)) 
      /(a)             -> /(a)

Source: ~sorreg-namtyv (2008d).

3.3 Nock 12K

Opcodes were reordered slightly. Compound opcodes were introduced, such as a conditional branch and a static hint opcode. Autocons appeared explicitly.

Author: Curtis Yarvin (curtis.yarvin@gmail.com) 
Date: 3/28/2008 
Version: 0.12 
 
51. Introduction 
 
    This file defines one function, "nock." 
 
    nock is in the public domain. 
10 
2. Data 
 
    A "noun" is either an "atom" or a "cell."  An 
    "atom" is an unsigned integer of any size.  A 
15    "cell" is an ordered pair of any two nouns, 
    the "head" and "tail." 
 
3. Semantics 
 
20    nock maps one noun to another.  It doesn't 
    always terminate. 
 
4. Pseudocode 
 
25    nock is defined in a pattern-matching 
    pseudocode, below. 
 
    Parentheses enclose cells.  (a b c) is 
    (a (b c)). 
30 
5. Definition 
 
5.1 Transformations 
 
35      *(a (b c) d) => (*(a b c) *(a d)) 
      *(a 0 b)     => /(b a) 
      *(a 1 b)     => (b) 
      *(a 2 b c)   => *(*(a b) c) 
      *(a 3 b)     => **(a b) 
40      *(a 4 b)     => &*(a b) 
      *(a 5 b)     => ^*(a b) 
      *(a 6 b)     => =*(a b) 
 
      *(a 7 b c d) => *(a 3 (0 1) 3 (1 c d) (1 0) 
45                          3 (1 2 3) (1 0) 5 5 b) 
      *(a 8 b c)   => *(a 2 (((1 0) b) c) 0 3) 
      *(a 9 b c)   => *(a c) 
 
      *(a)         => *(a) 
50 
5.2 Operators 
 
5.2.1 Goto (*) 
 
55      *(a)             -> nock(a) 
 
5.2.2 Deep (&) 
 
      &(a b)           -> 0 
60      &(a)             -> 1 
 
5.2.4 Bump (^) 
 
      ^(a b)           -> ^(a b) 
65      ^(a)             -> a + 1 
 
5.2.5 Same (=) 
 
      =(a a)           -> 0 
70      =(a b)           -> 1 
      =(a)             -> =(a) 
 
5.2.6 Snip (/) 
 
75      /(1 a)           -> a 
      /(2 a b)         -> a 
      /(3 a b)         -> b 
      /((a + a) b)     -> /(2 /(a b)) 
      /((a + a + 1) b) -> /(3 /(a b)) 
80      /(a)             -> /(a)