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