@@ -0,0 +1,274 @@
4+description = "The promise of Urbit lies in its reimagination of the digital world using components that are as constrained and limited as possible."
6+author = "Ted Blackman"
7+ship = "~rovnys-ricfer"
8+image = "https://media.urbit.org/site/posts/essays/hoon.png"
11+
13+### What can Hoon do that other languages can't?
15+The short answer is: implement a purely functional operating system.
16+Try to do this in a principled way in Haskell, and the problems you'll
17+run into will make design decisions in Hoon and Nock make a lot more
20+In particular, the problems Hoon solves that aren't solved by other
21+functional languages are:
22+- Compile and run other code in a typesafe manner at full speed,
23+- Typesafe metaprogramming, and
24+- Hot code reload and online data migration.
26+### What is Hoon good at?
28+Hoon is mostly good at compiling and running other Hoon code. Urbit
29+consists of many layers of bootstrapping. Several of these layers lean
30+heavily on this feature, including the Gall application runner, the Ford
31+build system, the Dojo shell, and the Arvo kernel itself. Even Urbit's
32+chat application lets you run Hoon expressions and share the results
35+### Why did we write the OS in Hoon?
37+The chain of reasoning goes something like this:
39+Software complexity leads to monopolies and lack of individual digital
40+sovereignty, in addition to bugs and security vulnerabilities. One of
41+the best ways to reduce software complexity is to restrict oneself to
42+pure mathematical functions — no side effects, no implicit arguments.
43+This makes the system deterministic. So we want a deterministic,
44+functional operating system for individuals to run.
46+This operating system should also be axiomatic; we don't want it to
47+depend on various idiosyncrasies of whatever the current hardware is
48+like. Hardware changes over time, and we want people to be able to pass
49+their computers on to their grandchildren, so we should have a virtual
50+machine that runs this functional operating system.
52+As hardware changes, people need to move their virtual machines to new
53+hosts. This means there needs to be a standard way to serialize and
54+deserialize the VM state at any time. The easiest way to do this is by
55+storing an event log, just like a database, and writing each event to
56+that before emitting effects caused by it. Since we also need state
57+snapshots, every piece of data in the system, including runtime state,
58+needs to be serializable to a standardized format.
60+Because the VM will likely move from host to host many times, it needs
61+to be tractable to actually implement a VM correctly. This means the
62+system specification needs to be simple enough that it's clear whether a
63+VM is in fact correct. The x86_64 instruction set that runs most
64+servers has somewhere between 1300 and 4000 opcodes, depending on how
65+you count. Nock has 12.
67+Since Urbit is an operating system, its main purpose is to load and run
68+programs on behalf of the user. This means the system needs to be
69+really good at hot code reloading, self-hosting, metacircularity, and
72+There aren't any other languages out there that are purely functional,
73+purely axiomatic, performant enough for practical personal use,
74+universally serializable, and good at runtime metaprogramming. Nock is
75+Urbit's solution to these design constraints. Some Lisps come close to
76+meeting these criteria — and Nock is very Lisp-like — but no practical
77+Lisp dialects are nearly as pure or axiomatic as Nock.
79+### What is special about Hoon?
81+It's a purely functional systems language. Calling it a functional
82+analog of C is not too far off in several ways. Almost all code
83+throughout Urbit's kernelspace and userspace is written in Hoon.
85+### What properties does Hoon have? What type of language is it?
87+Hoon is a statically typed, purely functional, strictly evaluated
90+Hoon and Nock have several unusual properties:
92+- **Axiomatic**. Nock is a fully axiomatic computing system — no
93+ dependencies, no builtins, no hardware dependence — just pure math.
94+ The jet system gives this a practical level of performance.
96+- **Layered**. Nock is machine code designed for machines to run; Hoon is a
97+ programming language designed for people to use. Hoon layers over
98+ Nock in a very similar way to how C layers over machine code. Nock
99+ has no symbols; all programmer-facing variable names live in Hoon
100+ types. You can use raw Nock from Hoon, much like dropping down to
101+ assembly from within C. Hoon compiles to Nock with no "runtime
102+ system" — aside from subtree lookups, you could pretty easily compile
103+ most Hoon expressions by hand.
105+- **Minimal**. Urbit is ruthlessly minimalistic throughout the stack. Nock
106+ has only twelve opcodes, and Hoon's semantics are a very thin layer
107+ over Nock's. The only fundamental datatype in Urbit is the noun:
108+ either an arbitrarily large natural number, called an atom, or a pair
109+ of nouns, called a cell. This forms a binary tree with atoms at the
110+ leaves. Lists, sets, maps, queues, executable code, closures, ASTs,
111+ buffers, strings, floating-point numbers, and everything else in the
112+ whole programming environment are represented using just this data
115+- **Acyclic**. There are no cycles in nouns, since they're always trees, so
116+ there are no cycles in Nock's memory model. Pointer equality is not
117+ exposed to the programmer. In practical Nock implementations, all
118+ data structures are what are elsewhere called "functional" or
119+ "persistent" data structures, meaning they're immutable<sup>*</sup> and share
120+ structure wherever possible.
121+ <br/><small>*with the exception of "unifying
122+ equality", which some runtimes provide as an optimization</small><br/>
124+- **Homoiconic**. Code and data are represented the same way and can be
125+ converted to each other. Lisp dialects are also homoiconic, but Hoon
126+ and Nock are arguably even more so, since things like closures and the
127+ environment are just Nock trees. We even have a statically typed
128+ metacircular interpreter called <code>+mule</code>. We run userspace code
129+ metacircularly with negligible performance overhead because of Urbit's
130+ jet system. In Lisp "eval is evil" is a common saying but, in Urbit,
131+ eval is a first-class feature.
133+- **Universally serializable**. There's one serialization format, called
134+ "jam", for any piece of code or data in the system. This makes it so
135+ that deserialization has just one function, a few hundred lines of C,
136+ as its security attack surface. It also facilitates portability of
137+ the virtual machine state, and it turns out to be useful in a bunch of
138+ places in the system.
140+- **Jetted**. A jet is a piece of code that the Nock interpreter has that
141+ reimplements a Nock function in some other, faster language. The `+dec`
142+ decrement function in Hoon's standard library is defined axiomatically
143+ using recursion, but is run as a jet written in C that makes use of
144+ the processor's ALU for performance. When calling a Nock function, if
145+ the runtime has a matching jet, it will use that instead of the Nock
146+ implementation. Nock isn't as slow as you might think, especially
147+ considering it's a minimal, dynamic, axiomatic language.
149+ This arrangement has the deeper implication that all code written in
150+ Nock is best considered as a specification for a program, which can be
151+ executed directly but might never run at all due to being jetted.
152+ Cryptographic functions, for example, should all have jets with
153+ constant-time implementations to prevent timing attacks. Most jets,
154+ though, just take advantage of hardware acceleration for things like
155+ floating point arithmetic.
157+- The amount of Hoon syntax is unusually large, but also **unusually
158+ regular**. Hoon is a "runic" language, meaning expressions generally
159+ begin with a digraph "rune" corresponding to the type of expression.
160+ Runes are used in place of keywords and Lisp's "special forms".
161+ Hoon's syntax makes better use of screen real estate than Haskell or
162+ Lisp by having a mostly vertical "backbone" of runes that prevents
163+ long functions from indenting repeatedly and helps quickly identify
164+ control flow. Hoon does not allow syntactic abstraction, so you
165+ always know exactly what you're looking at when reading Hoon. The
166+ similarity of Hoon's syntax to its abstract syntax tree makes
167+ metaprogramming easier and can be thought of as another layer of
168+ homoiconicity on top of Nock's.
170+- **Subject-oriented**. There is no implicit environment; a Hoon expression
171+ compiles down to a Nock formula, which is interpreted as a function
172+ that runs with the "subject" as the argument. The subject can be any
173+ Nock tree, but it contains everything that's in scope. It usually
174+ consists of the Hoon compiler and standard library as a stack of
175+ cores, along with whatever functions and variables have been defined
176+ in the lexical scope.
178+- **Cores**. A core is a pair of code and data. The core is the underlying
179+ representation of a function (a lambda with implicit fixed point), a
180+ library or module, an OOP-style object, and an OOP-style "interface"
181+ or "protocol". The code consists of a set of Nock formulas that can
182+ each be run against the whole core as a subject. This means there's
183+ always an implicit fixed point when running a function, and mutual
184+ recursion can occur among a core's formulas. A core's data usually
185+ consists of the standard library (itself a stack of cores), and
186+ possibly a "sample" (function argument).
188+- **The type system has several unusual features**. It's intentional, in
189+ the sense that all constructs are first-class and can be down-cast to
190+ `noun`, Hoon's "any" or "top" type that matches all Nock nouns. Types
191+ are also used as scopes, so they store all of Hoon's variable names
192+ and docstrings. The type system uses an unusual macro-like feature
193+ called "wetness" to implement parametric polymorphism. The type
194+ system can also auto-generate coercion functions that validate and
195+ lift raw nouns into structural types, such as lists or cells. This is
196+ used to validate untrusted data, such as from the network.
198+- **Reflective**. The type of type is just a normal datatype in Hoon, and a
199+ lot of the system manipulates types. In particular, the `!>` rune, when
200+ applied to a piece of data, uses compile-time type reflection to
201+ produce something called a "vase": a pair of type and data, similar to
202+ a <code>Data.Dynamic</code> in Haskell, or a limited form of a dependent pair.
203+ Since the Arvo kernel does a lot of dynamic compilation, it uses vases
204+ to implement something akin to a dynamically typed language using
205+ Hoon. This allows for type-safe dynamic program loading, program
206+ execution, and data migration.
208+- **Inert**. Because Nock is purely functional, Hoon compiles to it so
209+ directly, everything is homoiconic, and Hoon is intensional, there's a
210+ very nice feeling that everything is just a stationary tree. There
211+ are no special objects that can't be manipulated; everything in your
212+ environment is just a subtree, and you could grab it and print it out
213+ if you wanted to. There's nothing like a "database handle",
214+ "websocket connection object", or other mystical constructs. The
215+ calmness of working with such inert building blocks is addictive, as
216+ many Hoon programmers will attest.
218+### Why is Hoon the way it is?
222+Urbit's principled minimalism simplifies all kinds of things at many
223+layers of the stack; for example, Urbit's linker, which is part of the
224+Ford build system, just conses together multiple libraries into a tuple
225+to form the compile-time environment for a source file. Universal
226+serialization means we can safely send arbitrary pieces of data to apps
227+on other ships without any more work than sending them to a local app.
228+Using an app called Aquarium that's about three hundred lines of code,
229+Arvo can run a whole fleet of other Arvos inside itself at full speed,
230+just like Docker, and perform a suite of deterministic end-to-end tests
231+on the OS as a whole.
233+Even Hoon's seemingly baroque syntax is extremely regular and an
234+unusually thin layer over the abstract syntax tree. It's designed to be
235+a power tool; learning the syntax takes some time, but you only have to
236+learn it once, and then it's not hard to read. It's like an English
237+speaker learning Hiragana or Cyrillic. This heaping spoonful of syntactic sugar
238+(along with jets for performance) is enough to take Nock from a Turing
239+tarpit to a practical, ergonomic programming tool.
241+Subject orientation in Nock and Hoon stems partly from minimalism
242+(there's just one subject, which serves as state, lexical scope,
243+environment, and function argument), partly from a desire to simplify
244+compilation (the type of the subject is a full specification of the
245+compile-time environment for a source file), and partly in order to give
246+the language a more imperative feel.
248+You program Hoon as if you have a mutable environment, but you're
249+embedded in a purely functional, immutable context. While Hoon is a
250+purely functional language, many of its runes create a mutant copy of
251+the subject for manipulation by future runes (similar to Forth's stack
252+operations), which makes it feel more like an expression is "doing
253+something" rather than just calculating something.
255+Everything about a scope, including name bindings, aliases, and
256+docstrings, is stored in the subject's type. This allows Hoon's
257+compilation discipline to be similarly minimal: the compiler is a
258+function from subject type and Hoon source to product type and compiled
259+Nock. Running this Nock against a value of the subject type produces a
260+vase of the result. It's hard to imagine a more streamlined formalism for compilation.
262+The compilation discipline gets applied recursively to build the layers
263+of the Arvo stack. The Arvo kernel is compiled using the Hoon compiler
264+as subject, the Zuse standard library is compiled using the Arvo kernel
265+as the subject, and apps and vanes (kernel modules) are compiled using
268+The promise of Urbit lies in its reimagination of the digital world
269+using components that are as constrained and limited as possible. By
270+adhering firmly to principle and doubling down on minimalism at every
271+turn, we get an OS that provides far stronger guarantees than Unix with
272+a thousand times less code. Given the complexity of modern software,
273+this is what's required to put personal computing back into the hands of