language: en kae3g ← back to index
(unlisted) — This essay is not shown on the main index but remains accessible via direct link

kae3g 9503: What Is Nock? Specification Language for Sovereign Systems

Phase 1: Foundations & Philosophy | Week 1 | Reading Time: 18 minutes

What You'll Learn

Prerequisites

Helpful context:

The Specification Problem

Imagine designing an operating system that should last 100 years:

Problem: How do you specify what it should do?

Most OS specifications:

Result:

What if you could specify an entire OS in 12 rules?

That's Nock.

What Is Nock?

Nock is a combinator calculus: a pure function from noun to noun.

Translation:

nock(subject, formula) → product

Input:  Two pieces of data (subject, formula)
Output: One piece of data (product)

That's it. The entire specification.

Nouns: The Only Data Type

A noun is:

Examples:

Atom:     17
Cell:     [4 5]
Nested:   [[1 2] 3]
List-like: [1 [2 [3 0]]]

Everything is nouns: Programs, data, operating system state, all nouns.

Plant lens: Nouns are like cells (atoms = simple cells, pairs = tissue).

The 12 Rules (The Entire VM)

Don't memorize—just appreciate the radical minimalism:

Nock 4K Specification (12 reduction rules):

?[a b]           0               # cell test (yes)
?a               1               # atom test (no)

+[a b]           +[a b]          # increment crashes on cell
+a               1 + a           # increment atom

=[a a]           0               # equality (yes)
=[a b]           1               # equality (no)

/[1 a]           a               # tree addressing: root
/[2 a b]         a               # left branch
/[3 a b]         b               # right branch
/[(a + a) b]     /[2 /[a b]]    # even: recurse left
/[(a + a + 1) b] /[3 /[a b]]    # odd: recurse right

*[a [b c] d]     [*[a b c] *[a d]]  # nock of cell
*[a 0 b]         /[b a]             # slot
*[a 1 b]         b                  # constant
*[a 2 b c]       *[*[a b] *[a c]]   # nock (recurse)
*[a 3 b]         ?*[a b]            # cell test
*[a 4 b]         +*[a b]            # increment
*[a 5 b c]       =*[a b] *[a c]     # equality
*[a 6 b c d]     *[a *[[c d] 0 *[[2 3] 0 *[a 4 4 b]]]]  # if
*[a 7 b c]       *[*[a b] c]        # compose
*[a 8 b c]       *[[*[a b] a] c]    # extend subject
*[a 9 b c]       *[*[a c] 2 [0 1] 0 b]  # call
*[a 10 [b c] d]  #[b *[a c] *[a d]]     # hint
*[a 11 [b c] d]  *[[*[a c] *[a d]] 0 3] # static hint
*[a 11 b c]      *[a c]                 # dynamic hint

That's the entire virtual machine.

Compare:

Why This Matters for System Design

The Complete Sovereignty Stack

Vision (from the valley's architectural plan):

Your Sovereign System:
    ↓
Userspace Applications (Clojure + Nix)
    ↓ optimized by
GraalVM/TruffleVM (polyglot, JIT-optimized)
    ↓ reimplemented using
Nock as specification (abstraction layers provably correct)
    ↓ running on
Formally Verified Microkernel (seL4-style)
    ↓ specified in
Nock (12 rules - provably correct)
    ↓ executing on
RISC-V (open hardware)
    ↓ maintained via
Grainhouse Strategy (forked dependencies, total sovereignty)

Why Nock at MULTIPLE layers?

Layer 1: Kernel Specification

  1. Specification → Verification → Implementation
    • Write OS behavior in Nock (12 rules = formal spec)
    • Prove Nock spec correct (manageable size)
    • Implement in C/Rust (with proven correspondence)
  2. Auditable (security)
    • 12 rules = you can audit the entire foundation
    • Compare: Can you audit Linux? (30M lines)
    • Can you audit x86 microcode? (Proprietary!)
  3. Eternal (longevity)
    • Nock is frozen (never changes)
    • Write OS once, runs forever
    • No platform churn, no breaking changes
  4. Portable (sovereignty)
    • Nock runs on ANY architecture (x86, ARM, RISC-V, future CPUs)
    • Your OS isn't locked to one vendor's chips
    • True hardware independence

Layer 2: Userspace Language Runtime

Clojure + Nix as primary userspace languages:

Why Clojure?

Why Nix?

Current limitation: JVM is heavyweight, startup slow.

Solution: GraalVM + TruffleVM optimization!

GraalVM/TruffleVM: Fast Polyglot Runtimes

GraalVM = High-performance JVM with polyglot support

Key innovations:

Benefits for Clojure:

Standard JVM (HotSpot):
- Startup: 2-5 seconds
- Memory: 50-200 MB baseline
- Warmup: 30 seconds for full JIT

GraalVM (with optimization):
- Startup: 10-50 ms (native image)
- Memory: 5-20 MB baseline
- Warmup: Instant (AOT compiled)
- Performance: 2-10x faster (after warmup)

This makes Clojure practical for CLI tools, system utilities, embedded scenarios.

The Reimplementation Vision

Current state:

Clojure → JVM bytecode → JVM interpreter/JIT → Native code
         (complex, unauditable, 500K+ lines)

Proposed sovereignty stack:

1. Nock specification (12 rules)
   ↓
2. Clojure semantics in Nock (provably correct spec)
   ↓
3. Optimizing compiler (Nock → efficient native code)
   ↓
4. Verified runtime (minimal, auditable)
   ↓
5. seL4 microkernel (formally verified)
   ↓
6. RISC-V hardware (open ISA)

Goal: Replace JVM's 500K lines with:

Incremental path:

  1. Phase 1 (now): Use existing JVM/GraalVM (proven, works)
  2. Phase 2: Specify Clojure semantics in Nock (research)
  3. Phase 3: Build Truffle-style optimizer for Nock (performance)
  4. Phase 4: Verify compiler correctness (formal methods)
  5. Phase 5: Replace JVM entirely (full sovereignty)

Timeline: Phase 1 (today), Phase 5 (10+ years).

Why worth it:

Nock as Specification Language

Traditional approach (Linux, Windows, JVM):

1. Write C/Java code (implementation)
2. Test it (finite cases)
3. Hope it's correct (bugs everywhere)
4. Specification = "whatever the code does"

Nock approach (proposed for sovereign systems):

1. Write specification in Nock (12 rules = formal)
2. Prove specification correct (mathematical proof)
3. Implement in C/Rust/RISC-V (with verified translation)
4. Specification = immutable, auditable Nock code

Example 1: Process scheduling

Traditional (English spec):

"The scheduler should give each process fair CPU time, preempt after 100ms, and prioritize I/O-bound processes..."

Ambiguous! What's "fair"? How exactly does preemption work?

Nock spec (pseudocode):

[scheduler-formula
  [cpu-time-slice 100-ms]
  [fairness-algorithm round-robin]
  [preempt-check [0 current-time] [0 slice-start]]
  [io-priority-boost 10-percent]]

Example 2: Clojure persistent vector

Traditional (Java implementation):

// 500+ lines of complex array manipulation
class PersistentVector {
  Object[] array;
  int shift;
  // ... complex trie operations
}

Nock spec (mathematical definition):

[persistent-vector
  [structure balanced-trie-32-way]
  [lookup [index → value] O(log32 n)]
  [update [index value → new-vector] O(log32 n)]
  [structural-sharing 31/32-reuse-on-update]]

Precise, executable, provable.

The seL4 Connection

seL4 (the world's only formally verified OS kernel):

The problem: Verification of seL4 took 11 person-years.

The opportunity: If the specification were simpler (Nock's 12 rules instead of C semantics), verification becomes tractable.

Proposed architecture:

1. Nock specification (12 rules)
   ↓
2. Nock kernel (implements microkernel in Nock)
   ↓
3. Verified translation (Nock → C or Rust)
   ↓
4. Efficient runtime (with jets - fast C for verified Nock)

Result: Verified kernel with simple specification (Nock) instead of complex one (C).

Plant lens: Nock is the seed (genetic code), implementation is the plant (grown organism).

Minimalism Enables Verification

Why 12 rules matter:

Verification cost grows exponentially with specification complexity:

Spec SizeVerification Effort
12 rulesWeeks (feasible for small team)
100 rulesMonths (requires experts)
1,000 rulesYears (major research project)
30M linesImpossible (no one can verify Linux completely)

Nock's minimalism = verification becomes practical.

This is why military/aerospace systems use seL4 (10K lines) not Linux (30M lines).

Extend the logic: Nock (12 rules) → even simpler to verify than seL4!

The RISC-V Analogy

RISC-V philosophy: Minimal instruction set, open standard, extensible.

Base RV32I: 47 instructions (excellent minimalism!)

Nock philosophy: Even more minimal (12 rules), but same spirit:

Together:

Nock (software VM)  ←→  RISC-V (hardware ISA)
  12 rules               47 instructions
  Eternal spec           Open standard
  Provable               Auditable
  Portable               Vendor-neutral

Both enable: Long-term, sovereign, verifiable systems.

Practical Example: Nock in Action

Tree Addressing

Problem: Access nested data without variable names.

Nock solution: Binary tree addressing by slot number:

Subject: [[4 5] [6 [14 15]]]

Tree structure:
        root (slot 1)
       /              \
    [4 5]          [6 [14 15]]
   slot 2           slot 3
   /    \           /      \
  4      5         6     [14 15]
slot 4  slot 5  slot 6   slot 7
                          /    \
                        14      15
                      slot 14  slot 15

Access:

/[1 subject] → [[4 5] [6 [14 15]]]  (root)
/[2 subject] → [4 5]                 (left)
/[6 subject] → 6                     (left of right)
/[14 subject] → 14                   (deep nested)

Why this matters: No variable names = no scope issues, no shadowing, no closures to track.

Perfect for formal verification (simpler semantics).

How Nock Could Specify a Microkernel

Microkernel responsibilities:

  1. Memory management (virtual address spaces)
  2. Inter-process communication (IPC)
  3. Thread scheduling
  4. Hardware abstraction (devices)

Nock specification (conceptual):

# Memory allocation
[alloc-memory
  [size [0 requested-bytes]]
  [available-pages [0 free-list]]
  → [new-page-capability]]

# IPC send
[ipc-send
  [endpoint [0 target-endpoint]]
  [message [0 message-data]]
  → [send-result]]

# Scheduler
[schedule-next
  [ready-queue [0 runnable-threads]]
  [current-time [0 clock]]
  → [next-thread-to-run]]

Each operation: Pure function (noun → noun).

Benefit: Can prove properties:

This is the dream: Microkernel specified in 12 rules, then proven correct.

The Grainhouse Strategy Connection

From the valley's final vision (sovereignty architecture):

Grainhouse = Forked dependencies, maintained independently.

Nock fits perfectly:

Example grainhouse:

~/grainhouse/
  ├─ nock-vm/          # Your Nock interpreter (C or Rust)
  ├─ nock-kernel/      # Microkernel specified in Nock
  ├─ sel4-fork/        # seL4 microkernel (comparison)
  ├─ riscv-toolchain/  # RISC-V compiler
  └─ documentation/    # Every design decision documented

Result: Complete sovereignty (no external dependencies, all auditable).

Hands-On: Understanding Nock

Exercise 1: Noun Construction

Build these nouns:

1. Atom: 42
2. Cell: [7 8]
3. Nested: [[1 2] [3 4]]
4. List: [1 [2 [3 0]]]  (like Lisp cons)

Question: How would you represent a string?

Answer: List of character codes:

"hi" → [104 [105 0]]
       (104='h', 105='i', 0=end)

Everything is atoms and cells. No special types.

Exercise 2: Simple Nock Evaluation

Evaluate: *[[42 17] 0 2]

Step through:

  1. Rule: *[a 0 b] → /[b a] (slot addressing)
  2. Apply: *[[42 17] 0 2] → /[2 [42 17]]
  3. Tree address: slot 2 = left branch
  4. Result: 42

Try: *[[42 17] 0 3] (answer: 17 - right branch)

Exercise 3: Constant Formula

Evaluate: *[100 1 999]

Step through:

  1. Rule: *[a 1 b] → b (constant - ignore subject)
  2. Apply: *[100 1 999] → 999

Insight: Subject (100) ignored. Formula [1 999] always returns 999.

This is how you return constants (like return 42; in C).

Why Not Just Use Lambda Calculus?

Good question! Lambda calculus is also minimal.

Lambda calculus:

(lambda (x) (+ x 1))  ; function with variable x

Problems for verification:

Nock advantages:

Trade-off: Nock is less intuitive (no familiar variable names), but easier to prove correct.

For 100-year OS specification: Correctness > familiarity.

Criticisms and Honest Trade-offs

Nock is not perfect. Let's be clear:

1. "It's Slow"

True. Naive Nock is ~1000x slower than native code.

Solution: Jets (replace verified Nock with fast C when semantics match).

Status: Mature jetting → acceptable performance.

Priority: Correctness > speed (for kernel specification).

2. "Ecosystem is Tiny"

True. ~1,000 developers (vs millions for Linux).

Counter: Early adopters shape the future (Unix was tiny once).

Our position: Use Nock for specification, implement in proven languages (C/Rust).

3. "Unfamiliar"

True. Tree addressing is weird, no variables is alien.

Counter: Specification doesn't need to be familiar—it needs to be correct.

Analogy: Assembly is unfamiliar too, but CPUs use it (it's correct).

The Complete Valley Vision

Our multi-layer synthesis:

Foundation (Hardware → Kernel)

  1. RISC-V = Open hardware (vendor-neutral, auditable)
  2. Nock = Specification language (12 rules, eternal)
  3. seL4-style kernel = Verified microkernel (specified in Nock)

Runtime (Userspace Languages)

  1. Clojure = Primary application language (homoiconic, functional, practical)
  2. Nix = System configuration language (declarative, reproducible)
  3. GraalVM/Truffle = High-performance runtime (today's optimization)
  4. Nock-based compiler = Future reimplementation (auditable, verifiable)

Strategy (Independence)

  1. Grainhouse = Forked dependencies (every critical component maintained)
  2. Documentation = Every design decision recorded (knowledge sovereignty)
  3. Eternal = 100-year perspective (frozen foundations, evolutionary layers)

Together → Sovereign, verifiable, performant, eternal systems.

Phased Implementation

Phase 1: Today (Use proven tools)

Applications: Clojure (on JVM/GraalVM)
Configuration: Nix (declarative system management)
Kernel: Linux (with seL4 research)
Hardware: x86/ARM (with RISC-V migration plan)
Strategy: Begin grainhouse (fork critical deps)

Phase 2: 2-5 years (Bridge technologies)

Applications: Clojure (GraalVM native image)
Configuration: Nix (refined grainhouse)
Research: Clojure semantics specified in Nock
Kernel: seL4 or verified microkernel
Hardware: RISC-V available, migrate gradually

Phase 3: 5-10 years (Verified stack)

Applications: Clojure (Nock-based compiler, verified)
Configuration: Nix (all deps in grainhouse)
Kernel: Nock-specified, formally verified
Hardware: RISC-V (open fabrication available?)
Achievement: Fully sovereign, auditable stack

Phase 4: 10+ years (Generational stability)

Applications: Mature Nock-Clojure ecosystem
Configuration: Stable Nix grainhouse (decades old)
Kernel: Proven microkernel (zero exploits)
Hardware: Multiple RISC-V vendors
Legacy: Systems last 100 years

We're not saying "rewrite everything in Nock tomorrow" (impractical).

We're saying:

  1. Use Clojure+Nix today (proven, productive)
  2. Specify critical systems in Nock (security-critical kernel, runtime)
  3. Optimize with GraalVM (performance today)
  4. Reimplement gradually (Nock-based compiler, verified over decades)
  5. Achieve sovereignty incrementally (grainhouse strategy)

Plant lens:

The 100-Year Perspective

Curtis Yarvin (Nock's creator) asked:

"If you were designing software to last 100 years, what would you do differently?"

Traditional answer: Pick stable languages (C), avoid trends.

Nock answer: Freeze the foundation (12 rules, eternal), evolve everything else on top.

Comparison:

ApproachFoundation100-Year Outlook
LinuxC + POSIXConstant churn, security patches, breaking changes
Nock12 frozen rulesFoundation never changes, apps evolve
x86Growing ISACompatibility nightmare, legacy bloat
RISC-V + NockMinimal, frozenClean slate, provable, eternal

The valley chooses: Frozen foundations, evolutionary growth.

Try This

Exercise 1: Count Complexity

Compare specifications:

Reflect: Which could you audit? Which could you verify?

Which would you trust for a 100-year system?

Exercise 2: Design a Nock-Specified System

Task: Sketch how you'd specify a simple OS in Nock.

Components:

  1. Process management (create, destroy, schedule)
  2. Memory management (allocate, free, map)
  3. IPC (send, receive, synchronize)

Approach: Each as a pure function (noun → noun).

Example:

[create-process
  [executable-code [0 program-noun]]
  [initial-memory [0 memory-size]]
  → [process-capability]]

Insight: Pure functions = easier to verify, easier to test.

Exercise 3: Explore GraalVM Clojure

Try GraalVM native image with Clojure:

# Install GraalVM
sdk install java 21.0.1-graal

# Create simple Clojure script
cat > hello.clj <<EOF
(ns hello)
(defn -main [& args]
  (println "Hello from Clojure!"))
EOF

# Compile to native image
native-image --language:clojure -jar hello.jar hello

# Run (notice startup time!)
time ./hello
# Output: 10-50ms (vs 2-5 seconds on standard JVM)

Observe: GraalVM makes Clojure practical for system tools.

Question: Could we build this optimization layer on Nock semantics instead of JVM bytecode?

Exercise 4: Design Nock-Based Language Runtime

Task: Sketch how Clojure semantics could be specified in Nock.

Components:

  1. Persistent data structures (vectors, maps, sets)
  2. Function application (with closures)
  3. Lazy sequences (delayed evaluation)
  4. Concurrency primitives (atoms, refs, agents)

Approach: Each as pure Nock formula (noun → noun transformations).

Challenge: How do you represent time (for concurrency)?

Hint: Nock is deterministic → time must be explicit input (like game frame counter).

Going Deeper

Related Essays

External Resources

Reflection Questions

  1. Is 12 rules too minimal? (Or is complexity the enemy of correctness?)
  2. Can you verify a system you can't hold in your head? (Linux = 30M lines)
  3. Should specification and implementation be separate? (Or is "code as spec" acceptable?)
  4. What would 100-year software look like? (Frozen foundation? Evolutionary layers?)
  5. Is formal verification worth the cost? (11 person-years for seL4—but zero exploits since 2009)

Summary

Nock is:

Key Insights:

Complete Valley Stack:

Layer 1 - Foundation:

Layer 2 - Runtime:

Layer 3 - Strategy:

Implementation Path:

  1. Today: Clojure+Nix on JVM/GraalVM (productive)
  2. 5 years: Clojure semantics specified in Nock (research)
  3. 10 years: Nock-based Clojure compiler (verified, fast)
  4. Generations: Stable, sovereign, auditable stack

In Practice:

Plant lens:

Next: We explore Clojure—a practical, modern Lisp that brings Nock's "code as data" philosophy to the JVM and JavaScript, with a thriving ecosystem and proven track record.

Navigation:
← Previous: 9502 (ode to nocturnal time) | Phase 1 Index | Next: 9504 (what is clojure)

Bridge to Sovereignty: For the complete vision, see:

Metadata:

Copyright © 2025 kae3g | Dual-licensed under Apache-2.0 / MIT
Competitive technology in service of clarity and beauty

← back to index