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