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