Wednesday, January 13, 2010

Urbit: functional programming from scratch

Urbit is a static functional namespace: a programming environment specified as a single stateless, frozen function. The Urbit function is Maxwellian: formally defined by a small system of axioms. Urbit, while a cool toy, is designed for practical computing.

If this sounds like it needs some explaining, it does. But first, since Moron Lab is just a blog and not a recipient of Federal funding, I can start with a vaporware disclaimer. Urbit, while all the things I say it is, does not exist. Indeed, it may never exist.

Urbit, which is vaporware, can indeed be described as a "static functional namespace." Or it could if it existed, which it does not. While Urbit is designed to be useful, it is only a design. Some of this design is complete; some is not. It is not in any sense useful at present, because it does not exist. It may be useful in future, or not. I expect the former; I believe in the former; but as Mandy Rice-Davies said, "well, he would, wouldn't he?" I have certainly not demonstrated it, and will not any time soon.

That said: a what? What in the bejesus am I peddling here? What percentage is real, what percentage is vapor? What does it do, why does it do it, and when will it do it? Most important: what problem is it supposed to solve?

Since these are always the questions I ask when introduced to someone else's random vaporware, it seems sensible to ask them of myself. It seems impolite to suddenly start spouting technology. Besides, as we'll see, there is really not a lot of technology here. Context must always come first.

You may also be interested in about comparable efforts for defining software from the bottom up, such as Kay and Piumarta's work at VPRI, or Paul Graham's Arc. This list should probably be longer - if you know of any other active effort that should be on it, please notify. If non-active efforts were included, the list might exceed Blogger's disks. The problem, by definition, is not a new one.

If you follow those links, you'll see that everyone has their own introduction to "software from scratch." So, of course, do I. Mine starts with Mars.

Few of us have been to Mars. But science fiction has filled in many of the gaps. We know that the Martian civilization is immensely old. Its software technology, therefore, must be similarly antique. Obviously nothing like it exists on earth - though those of us who remember VMS might be deceived.

Whether we remember VMS or not, some of us are unhappy with the state of Earth software. Therefore it behooves us to consider an alternative. Since we have not yet established communications with the Martians (who retreated into tunnels as their planet froze), we cannot just FTP their code. We could, however, try to write it.

What is Martian code actually like? There are two possibilities.

One: since Earth code is fifty years old, and Martian code is fifty million years old, Martian code has been evolving into a big ball of mud for a million times longer than Earth software. (And two million times longer than Windows.)

This hypothesis strikes me as possible, but implausible. Since the big ball of mud expands indefinitely, Martian code would therefore be so large and horrible that, despite its underground installed base, the server room bulged into space like a termite mound, intercepting low-flying asteroids and stinking up the solar system all the way to Pluto. Our latest space telescopes would surely have detected this abominable structure - if not, in fact, collided with it.

Two: therefore, at some point in Martian history, some abject fsck of a Martian code-monkey must have said: fsck this entire fscking ball of mud. For lo, its defects cannot be summarized; for they exceed the global supply of bullet points; for numerous as the fishes in the sea, like the fishes in the sea they fsck, making more little fscking fishes. For lo, it is fscked, and a big ball of mud. And there is only one thing to do with it: obliterate the trunk, fire the developers, and hire a whole new fscking army of Martian code-monkeys to rewrite the entire fscking thing.

This is such an obvious and essential response to the big ball of mud pattern that, despite the fact that we know nothing about Mars, we can deduce that it must have happened on Mars. Probably several times. Probably several hundred. For each of these attempts but the last, of course, the result was either (a) abject failure, (b) another big ball of mud, or (c) both.

But the last, by definition, succeeded. This is the crucial inference we can draw about Mars: since the Martians had 50 million years to try, in the end they must have succeeded. The result: Martian code, as we know it today. Not enormous and horrible - tiny and diamond-perfect. Moreover, because it is tiny and diamond-perfect, it is perfectly stable and never changes or decays. It neither is a big ball of mud, nor tends to become one. It has achieved its final, permanent and excellent state.

For instance (and just for instance - this is by no means a guarantee of perfection), Martian code is entirely Maxwellian: computationally defined by a small set of axioms. In other words, it is formally specified - always and everywhere. Nothing else could be perfect.

Of course, Martian code is also Martian. So completely incompatible with Earth code. Note, however, that Mars had to go through this same transition - they had to throw away their old Windows for Mars (tm), and adopt this new, tiny, diamond-perfect kernel.

But can Earth code cooperate productively with this alien intruder? It sure can. All it takes is glue - and Earth code is no stranger to glue. If there's one thing Earth doesn't need, it's a new glue language. There is certainly no difficulty in gluing Mars code to Earth code. From the Earth perspective, Martian software is just another strange, mutually incompatible doohickey. Welcome aboard! Alas, our mudball is already ornamented with many such curios. They stick quite well.

Moreover, Martian code is so perfect that it cannot be contaminated, even in this sticky environment. The general structure of cross-planet computation is that Earth always calls Mars; Mars never calls Earth. The latter would be quite impossible, since Earth code is non-Maxwellian. There is only one way for a Maxwellian computer to run non-Maxwellian code: in a Maxwellian emulator. Any direct invocation is an implementation error by definition. Thus, Mars remains completely pure and Martian, even while glued firmly to Earth.

Unfortunately, Moron Lab is not in contact with Mars and cannot download their tiny, diamond-perfect, 49-million-year-old kernel. Therefore, we have had no alternative but to construct our own. It is not entirely done yet, and even the done parts are probably nowhere near the quality of real Martian software. Getting them there will require an actual collective effort, in the traditional open-source manner. Instructions for participation are at the end of the post.

As with any dangerous new technology, it's fortunate that Urbit is not yet fully armed and operational. It's our plan to introduce Martian computing gradually, to avoid producing serious social unrest. He who controls the spice controls the universe. While Martian code is not in any real position to dominate the universe, it cannot be described as Martian with a straight face, unless clearly designed to dominate the world. After all, it's already dominating Mars!

Any ersatz, Earth-produced Martian code is truly Martian in character only if it is obviously and self-evidently immune to any extension or improvement. Simplicity inflation is a chronic industry disease; Martian software must be far beyond simple. It can only be described as stupid in its majestic triviality. Or, of course, moronic.

Last week, we saw the Martian computational automaton, Nock. (Or, in the original Martian, Nwoglecq.) I posted the spec of Nock - but I didn't say what it was for. Today, we'll see what it's for.

Let's start by taking a closer look at the Martian data structure: the noun. Broadly, this is the Martian equivalent of XML, JSON, or S-expressions. Here is the definition:
A noun is either an atom or a cell. An atom is an unsigned integer of any size. A cell is an ordered pair of any two nouns.
Doesn't this data structure strike you as Martian (or moronic) in quality? Some readers may say: yes, obviously. This is the Martian data structure. Others may not be so sure.

Let us, therefore, defend this structure - the noun. We'll see why it's absolutely minimal and perfect. To validate the exercise, we'll forget Mars for a moment, and explain nouns in mere Earth terms.

First, we note that nouns reflect no concern whatsoever with the fascinating problem of deriving mathematics from propositional logic, set theory, etc. The unsigned integer, or natural number, is boldly and uncritically adopted as an axiomatic feature of the universe - as is the even more speculative ordered pair. Unlike the lambda calculus, Nock represents code as data, not data as code. This is because it is system software, not metamathematics. Its loyalties in this matter are not even slightly divided.

The Earth software that's most like Martian software is, of course, Lisp. (Lisp claims to be based on lambda, but the connection is in fact dubious - a true lambda language is more like Haskell.) Nouns can be described as "S-expressions without the S" - that is, there are no symbols or other base types; atoms are completely typeless. Note that Rivest's IETF draft also makes this change, although he (a) defines his atoms as octet-strings, not unsigned integers; and (b) remains list-centric, not pair-centric.

Of course, an octet-string and an unsigned integer are the same thing. And by general convention and common decency, nouns are pair-centric. In Nock, it is bad form to stick unnecessary terminators on tuples. Or, as a Lisper would say, "improper lists." Other than these unfortunate articles of baggage, though, Rivest's draft has a lot of cool syntax, which could easily be adapted to nouns and probably should be - if just to quell the suspicion, perhaps already pregnant in your mind, that Urbit is really just the world's worst case of NIH syndrome.

Note, however, that there is no textual language definition associated with nouns. There is no one "noun syntax." There will never be. We define the data structure, not the syntax. A remarkable variety of functions map invertibly between an atom (such as a text file) and an arbitrary noun. Except for standardization reasons, there is no reason to privilege any one such function. And as for standardization, Urbit's approach will shortly be clear!

Note the similarity of nouns to the Unix file abstraction. An atom is actually slightly cleaner than a Unix bytestream, because an atom's size in bits is data, not metadata. (From the bytestream perspective, direct atomic encoding ignores trailing null octets.) And of course, because nouns also have cells, they can represent actual data structures directly - without encoding.

Nonetheless, if you look at pre-Unix OS, you see filesystems festooned with an enormous and inordinate variety of built-in file-type mechanisms. One of the greatest achievements of Unix was to take out all typed records and shoot them. Unfortunately, Unix did not provide for type at a higher layer, but it inevitably crept back in as filename extensions and MIME types. Extension and MIME together are not exactly the world's best type system, especially as there is no formal specification of a MIME type. But they work.

So it's not that Unix has no type system. It's that it has a layered type system. A MIME type specifies a set of files - at least, a good MIME specification can be converted, typically with nontrivial human effort, into a boolean predicate function which tells you whether a typeless bytestream is or is not, say, a GIF. Because the generic data model (bytestreams) is not cluttered with quixotic attempts at defining image formats, the description layer remains clean.

Nouns are designed on this principle. For instance, while nouns have no string type, any string is an octet-string, and any octet-string is an unsigned integer, ie, an atom (conventionally LSB first). Because there is no way to tell whether an atom is an integer, a string, or something else, printing an untyped noun is at best a delicate and heuristic process. Of course, so is printing an untyped Unix file.

Adding a string type seems like a very simple improvement to nouns. In fact it would be a disaster. For instance, what character set are the strings in? Unicode? Great. You've just taken a data model defined in three sentences, and expanded it to a shelf-sized manual set. If you have a shelf that strong, why not just start with VMS? Or, of course, you could include some simple, broken, built-in string type, in which case you're making the same mistake that VM/370 made with its record formats: inserting a low-level facility which higher layers will (or should) work around, not with.

Moreover, note that nouns are acyclic. In my own personal opinion, the task of constructing formal descriptions of cyclic data structures is one of the most substantial wastes of human brainpower since Thomas Aquinas was a little boy. Like the Revelation of St. John the Divine, the foundations of mathematics, or the classification of butterflies, this problem appears capable of absorbing arbitrary human intelligence in both quality and quantity.

So why does Earth use cyclic data structures, and why doesn't Mars? This demands a digression on Nock and performance.

Cyclic pointer graphs are, of course, essential to the high performance of low-level programming languages, such as C. There is no C on Mars, but there is something quite like it. It is not difficult to define a low-level language in functional, Maxwellian terms: just model an address space as an atom, and iterative mutations of that address space as processing steps. If you define a C interpreter this way, you have a functional definition of C - which need not be executed by naive iteration. But I digress.

The point is: if your goal is merely to model data, you neither need nor want cyclic graphs nor pointer identity. (Note that while nouns containing replicated subtrees can and should be represented physically as acyclic graphs, there is no Nock operator, like Lisp eq, which reveals pointer identity.) Nor are cyclic structures required to specify any interesting algorithm.

Rather, pointer cycles are useful only for efficient implementations of certain algorithms. Which is not nothing. However, it suggests an approach to optimized noun processing. Specify your entire program in functional, Maxwellian code; if this is not fast enough, implement key functions in C.

These C functions, or jets, will take noun arguments and produce noun results. In between, they can do whatever the heck they want - so long as they produce the same result as the actual Nock formula. They can even make system calls and have side effects, though this is a very bad idea. A jet is not a "native method."

The assumption that any practical Nock interpreter will be optimized for the specific formulas it is expected to execute, jet-propelling all well-known inner loops, allows Nock to discard many programming-language features normally considered essential to efficiency - from cyclic graphs, to built-in arithmetic. Because its only arithmetic operator is increment, decrement in Nock is an O(n) operation. But this is not a practical concern, because a production Nock interpreter will recognize the standard decrement formula and substitute an efficient jet. The approach is quite scalable.

Thus the design narrative for nouns. The result is a design that could have been invented in 1960 - and, in various forms more or less corrupt, has been invented umpteen times since 1960. However, it also clearly benefits from 50 years of programming history, and it seems to satisfy Saint-Exupéry's principle. Martian code may not always be this clean, but it should at least try to be.

Your reaction to nouns may be: but does it need to be this clean and simple? Yes. It does. This is perhaps my most significant objection to "other peoples' languages." They all want to be clean and simple. Everyone does. But their idea of clean and simple: terminating bacterial growth. My idea of clean and simple: terminating atomic motion.

Which is not because, like Sir James Dewar,
Sir James Dewar
Is a better man than you are
None of you asses
Can liquefy gases
I'm a better man than they are. It's because I have a different problem to solve. If mine can be solved at all, which is not at all clear, it can be solved only at cryogenic temperatures.

In case this metaphor is too weird for you, let me make it concrete. Normally, when normal people release normal software, they count by fractions, and they count up. Thus, they can keep extending and revising their systems incrementally. This is generally considered a good thing. It generally is.

In some cases, however, specifications needs to be permanently frozen. This requirement is generally found in the context of standards. Some standards are extensible or versionable, but some are not. ASCII, for instance, is perma-frozen. So is IPv4 (its relationship to IPv6 is little more than nominal - if they were really the same protocol, they'd have the same ethertype). Moreover, many standards render themselves incompatible in practice through excessive enthusiasm for extensibility. They may not be perma-frozen, but they probably should be.

The true, Martian way to perma-freeze a system is what I call Kelvin versioning. In Kelvin versioning, releases count down by integer degrees Kelvin. At absolute zero, the system can no longer be changed. At 1K, one more modification is possible. And so on. For instance, Nock is at 9K. It might change, though it probably won't. Nouns themselves are at 0K - it is impossible to imagine changing anything about those three sentences.

With these basic conceptual tools in place, let's step back and design the Martian computing infrastructure. We have already started to look at it from one perspective: from the axioms up. Let's refocus and take a different angle: from the network in.

Strangely enough, some insight into Martian networking can be gleaned by reading this Wikipedia page, or watching this Van Jacobson talk. (VJ, in case you're not aware, is a god in human form.) When I saw the latter I thought: "that bastard had my idea!" "Bastard" was not actually the word. It was a worse word - illegal, in fact, in many states. But of course, any truly Martian idea is far too simple to be original. Fortunately, VJ did not have my whole idea - just the network part.

I call the Martian network architecture source-independent networking, or SIN. In almost every way, a source-independent network is exactly the same as today's insecure, unreliable packet network. However, there is one difference. To make IP source-independent, remove one 4-byte field: the packet source address.

In SIN, a packet's processing is independent of the sender. Its meaning must be computed from the packet itself. If you're not instantly convinced that this is right and good and true, watch the talk - VJ will tell you all about it. VJ more or less invented TCP, which is fundamentally source-dependent. So I'd kind of suggest you believe him on this one. It takes a true engineer to throw out his own mistakes.

On Mars, SIN is taken to an extreme. Logically, Urbit is a single broadcast network - a single big Ethernet wire. Everyone sees everyone else's packets. You don't send a packet. You "release" it. As a matter of practical optimization, of course, routing is necessary, but it is opaque to the receiver. If there is a routing envelope, it is stripped before processing.

An easy way to see this is to compare an Urbit packet, or card, to an IP packet. An IP packet has a header, which is visible both to the routing infrastructure and the application stack. The header, of course, contains the infamous source address. Urbit removes not just the source address, but also the rest of the header. An Urbit card is all payload - it has no region seen both by receiver and router.

A card is simply a naked atom - a large unsigned integer. Nothing about its internal structure can be assumed. Obviously, since Martian networking is insecure and unreliable, it may consist entirely of garbage. Anyone could have sent us this garbage. Moreover, whether a card is garbage or not, we can discard it for any reason at any level.

Of course, a card is not at all opaque or without structure. It would be a strange routing infrastructure indeed in which the routers never examined their payloads. But logically, a card is simply a naked PDU (as the old WAP specs used to put it - if you hear an individual using this term, while he may be a fine individual personally, in professional life he is the only thing worse than a Bellhead: a Euro-Bellhead; flight is indicated) in the Urbit protocol. Ie: an Urbit message, which can be delivered to any Urbit host, at any time, for any reason.

In Urbit, the function is the protocol. Which is also the application. On Mars, there is only one application: Urbit. There is one operating system: Urbit. There is one network protocol: Urbit. One ring to bind them all, and in the darkness hold them!

On Mars, Urbit is TCP, Urbit is HTTP, Urbit is Linux, Urbit is Java, Urbit is Tomcat, Urbit is Mozilla. Urbit is the entire application stack above the network layer, on both server and client sides. There is no pre-Maxwellian application logic presently executing on Mars, although a few of the darkest, most ancient histories allude vaguely to such abuses - just as in the oldest books of Judaism, we see hints of human sacrifice. (Urbit is actually dedicated to the Roman bull-god, Mithras.)

Below Urbit, as below any standard, is whatever it wants to be. On Earth: the classic American operating system. Presumably on Mars there is some classic Martian equivalent. Just as almost anything can run a Web browser, almost anything can compute Urbit.

Back to the network-up design. We have seen the network. Up to the computer.

The formal state of an Urbit computer is its deck: the list of cards it has received, newest first. Clearly, there is only one network on Mars. Just as clearly, there is no pre-network legacy I/O. Everything the computer knows, it knows because it received a card that told it so. Even time can (and should) be delivered by card.

Now, a small reality check. In practice, is it always practical for a computer to store all the packets it has ever received? In some cases, this is exactly what it should do. Disk space is much cheaper than network bandwidth. The ratio is only changing in the former's favor. In other cases, of course, storing the entire deck would be preposterous. Broadly, most servers should; most clients should not.

It is always practical, however, to define the computer's semantics as a function of its deck. Ideally, these semantics should be crafted so that computers not needing the whole deck can devise some hack to avoid storing it. In general, one of the great benefits of tightly-specified systems is that they can be safely hacked to within an inch of their lives.

But what is the function? Ah. Well, this is where the vaporware comes in. I don't have the Urbit function, you see. I have a description of the Urbit function - an interface. Eventually, I expect to implement this description. The result will receive a Kelvin number - probably about room temperature. When Urbit reaches 0K, it is done and frozen forever. This will be as soon as possible, and no sooner.

What does Urbit do? Urbit defines the functional semantics of a computer's deck. The deck is the computer's state; to compute, we must query it. This suggests an obvious interface, which I render in pseudo-C:
noun
Urbit(noun path, atom_list deck)
{
  return file;
}
In other words, the Urbit function is a functional namespace. This pure, stateless function takes two arguments, a name or path, which is an arbitrary noun; and a packet log or deck, which is a list of atoms. It returns a value or file, also an arbitrary noun. I trust that we are not far into rocket-science territory here.

The function can fail, of course. Like its computational automaton, Nock, Urbit is crash-only. All errors are modeled as nontermination - ie, an infinite loop. Of course, your actual implementation need not spin forever upon mandatory nontermination. It is just a way of saying that all computation ends, and no result is produced.

(This is generally referred to as an exit. An exit is like an exception, except without an exception object. If a Nock computation does not exit, but succeeds, it is said to pass. If it is aborted externally for failure to compute, it is said to tank. Thus a mandatory or formally detected infinite loop exits; a heuristically suspected infinite loop, or any other computation judged impractical, tanks.)

When Urbit passes a file for some path and deck, the path is said to be bound in that deck. When Urbit exits, the path is unbound. The path-deck-file triple is the binding.

Urbit is not just a functional namespace, however. It is a static functional namespace. That is: its definition ensures that for every binding
Urbit(path deck) == file
we also know
Urbit(path [card deck]) == file
In other words, once a binding is determined, new cards cannot revise it. Once Urbit learns something, it cannot un-learn it. A functional namespace obeying this property also could be described as monotonic, but I prefer the simpler static. Static namespaces, for instance, are common in revision-control systems - for obvious reasons.

I hope you'll agree that this problem definition is not rocket science. Surprisingly, however, the legitimate FP community (by which I mean the Haskell community) is still searching for it.

As Conal Elliott writes:
This perspective is what’s behind my confidence that we will someday really learn to look at whole systems in a consistently functional/denotational [style] (simple and precise semantics).
Read the whole thing. Haskell fans, you'll know exactly where you can stick your monads. Indeed, Elliott on monadic I/O sounds a lot like VJ on connection-oriented networking. This is not, I believe, a coincidence. If Urbit is like anything, it's like Elliot's FRP - though with no monads, gonads, morphinisms, monoids, combiguators, or other implements of metamathematical torture.

Now, let's step back a moment and look at the most important aspect of the Urbit function. The most important aspect of the Urbit function is that it is frozen. It is nothing special to write a function which maps path and deck to file. It is something else to freeze one. Everyone on Mars uses the same Urbit, and has for 49 million years.

It is also something else to make that function universal. Mars has no computational infrastructure other than Urbit. Code on Mars is of two types: code within Urbit, and implementations of Urbit. In practice, this means that Urbit has to be able to do anything any application can do, and do it well.

So we have the Urbit problem: a frozen, universal, static functional namespace. In other words: a standard static functional namespace. Perhaps we are getting further into the rocket-science department. It is not hard to write a functional namespace. But how can we standardize a functional namespace? You will search the RFC Editor's shelves in vain for anything even remotely like Urbit.

In general, IETF RFCs and things like them (IETF is at the top of a tall food-chain of Internet standards organizations, descending in quality) do not standardize functions. When they have to standardize functions, they do not use any existing programming language. They use pseudocode - in other words, informal English. This is not out of stubbornness or stupidity - it is exactly the right thing to do.

The problem is a mismatch in objectives between the people trying to standardize languages, and the people trying to standardize protocols. There is simply no Turing-complete function definition format that is small and stable enough to reference as a dependency in an RFC. If you're writing an RFC, here is the type of external standard you want to depend on: ASCII. Even XML is a bit dodgy. But even a "simple" practical language like Scheme is defined by a 50-page manual. Show me a 2-page spec that depends on a 50-page spec, and I'll show you a 52-page spec.

In an RFC, pseudocode or English is better than Scheme, because Scheme would give a false impression of precision. Scheme is defined by an old-school language-standardization process whose goal is to terminate bacterial growth. Internet standardization means terminating atomic motion. Scheme seems pretty cool to Schemers, but it's nowhere near chilly enough for Urbit.

Urbit, of course, is defined by a Nock formula:
Urbit(path deck) == Nock([path deck] urbit-formula)
Since Nock is specified in less than 200 words of English, so is Urbit. The formal precision of Urbit is the formal precision of Nock. The formula does not add to this total - it is code, not English. And Nock, I think, is about as precise as a practical automaton can get.

Of course, this urbit-formula noun is not at all a pretty thing - a large (though not vast - certainly measured in kilobytes, not megabytes) tree of 0's and 2's and 3's. The definition of Urbit is certainly precise, because Urbit is defined in Nock, and Nock is precise. However, since it is not easy to write a big tree of small numbers, surely it is quite impossible for everyone to agree on a big tree of small numbers. Standardization requires extreme clarity, whereas Nock formulas are extremely obscure.

Therefore, we need another deliverable: a human-usable language, Watt. Watt is defined as follows:
Watt(source) == Nock(source watt-formula)
Thus, for instance,
urbit-formula == Watt(urbit-source) 
              == Nock(urbit-source watt-formula)
watt-formula == Watt(watt-source) 
             == Nock(watt-source watt-formula)
In English, Watt is a self-compiling compiler that translates a source file to a Nock formula. Watt is formally defined by the combination of watt-source and watt-formula. The latter verifies the former. Again, we are not in rocket-science territory here.

To bootstrap Watt, we write Watt in C, then use that implementation to write Watt in Watt, then ensure the two are equivalent. Thus, we never have to write anything in raw Nock - and we never do. (Except as an exercise, of course.)

Thus, to agree on Urbit, here is what we need to agree on: the Nock spec, the Watt source, and the Urbit source. The Nock spec is pseudocode, but very short and already very cold. Watt and Urbit are Maxwellian source, both readable and well-defined. (Watt, of course, must be not just a usable language, but an excellent one.) They should also be small. Definitely under 5000 lines of Watt - ideally, under 2000. Anything much larger would be almost impossible to get to zero Kelvin. As it is, the task will be quite difficult.

Should this be submitted to an actual standards organization, such as IETF? Maybe, but maybe not. As a Marxist might say, the historical mission of the standards forum may be reaching its end. An even more challenging test for a proposed standard, such as Urbit, is that it be suited to standardization without a formal process. If it is hard to standardize a system through IETF, it is even harder to standardize it without IETF. Obviously, any challenge that forces Urbit to be more Martian is good for Urbit.

This poses an obvious question. Is this really possible? How in the world can a 5000-line program, in any language, constitute an entire planetary software infrastructure? We may be able to freeze Urbit - but can we make it universal?

If Urbit has any hope of universality, it has to do something else which is traditionally Not Done (tm). It has to run code off the network. To run code off the network is to extract a source tree, or other application representation, from the deck, and execute it within the Urbit function. Yikes!

It is easy to see that execution of remote code is an absolute requirement for any source-independent network. Since the network does not have a source address, it must validate packets through cryptography. Since no encryption algorithm is proven secure, any serious functional namespace must be able to upgrade its crypto algorithms. To validate packets secured by the new algorithms, it must run code that was delivered as data - secured by the old algorithms.

Again, we see why a new language is needed. The reason, as always, is a new problem. The only family of functional languages designed to execute code as data is the Lisp family. For instance, to write Urbit in Haskell, you would need a Haskell interpreter written in Haskell. It could be done, but I don't think it has been done; and Haskell is certainly not designed to do it well. Therefore, the revolution will not be Haskellized.

Most Lisps can compile and evaluate remote code. At least, if your Lisp can't, it is not much of a Lisp! However, I know of no Lisps designed to solve this problem. I also know of no Lisps which are anywhere near as frozen as Nock. Hence: a new language.

In case you're still wondering whether Urbit can actually serve as a frozen, universal programming environment, let's pull the camera back and examine this monster in the large.

Any Urbit computer may be described in three ways: by what it hears, what it knows, and what it does. By analogy to another famous TLA, we can call this the HKD model.

What the computer hears is the list of cards it has received - its deck. One computer, one deck. Not even the computer's identity is defined outside the deck. Its identity is a function of what it has heard, which is the deck. What makes a deck, say, Igor's deck? A deck is Igor's deck if it contains Igor's secrets. This enables it to decode Igor's email, display Igor's photographs, talk to Igor's bank, etc. Generally, it enables Urbit to compute Igor's applications.

What the computer knows is the Urbit namespace: the meaning of the deck. For instance, suppose your computer wants to display the front page of the New York Times. "The front page of the New York Times" is not a phrase that can be mapped to a static path. "The front page of the New York Times at 6:15:01 PM, January 12, 2010" is. Similarly, "the image on Igor's monitor" is not a static path; "the image on Igor's monitor at 6:15:01 PM, frame 12, pixel (653, 24)" is.

If Igor is reading the Times at that time, Urbit must know that Igor's monitor is showing an image that is a rendering of the Times front page as of that time. Of course, this requires Igor's deck to actually contain an up-to-date copy of the New York Times.

Which presumably requires Igor's computer to have contacted that of the Times, etc, etc. How does Urbit send cards? It only appears to receive them. Is it just half the protocol definition?

This gets us to the third part of the HKD model, which is what the computer does. Which is what? What does it do? Oddly enough, we haven't said anything about this at all.

Answer: what it does is its own damned business! Urbit is no more than a recipe for how to interpret cards. A computer must act; it is useless unless it causes some side effect, whether by actual, physical output, or just by releasing more cards. No standard can constrain its actions. All Urbit can do is to define the knowledge it needs to act; all it can hope is that this knowledge is computed by the Urbit namespace, not ad hoc in the traditional manner - or worse, by a competing functional namespace.

So, for instance, Igor is reading the New York Times. To display the Times, his computer must contain the Times. To get the Times, it must contact the Times. To contact the Times, it must release and route cards. In other words, Igor's browser application must know that, at some time T, Igor does not have the Times; Igor wants the Times; and Igor's browser, to satisfy this request, proposes to release certain cards, with envelopes that should route them to the Times. All this, Urbit can know.

Urbit can specify all this knowledge - or, to be more precise, compute it from Igor's deck, which presumably includes his keystrokes and mouse movements. But Urbit cannot do. Urbit cannot force an Urbit implementation to actually calculate Igor's browser requests, and route the resulting cards to the Times. It can define the calculation; it cannot cause it to happen, or cause the results to be used.

And that's all for this week. However big your brain is, I suspect it is probably full.

Next Thursday, we'll dig a little deeper into Urbit. Which is vaporware - but not as vaporous as this post might make it seem. In particular, although there are many enormous problems, both practical and theoretical, in making this architecture work, the most significant impediment is the problem of allocating the namespace. After all, since everyone on Mars is running the same function, they all have to share the same static namespace. One can imagine some conflicts.

Any good namespace allocation must solve the unsolvable problem known as Zooko's triangle. The problem is, of course, unsolvable. Therefore, Urbit does not and cannot solve it. However, in the classic OS style, we can score 100% on one vertex and 75% on the other two. This quasi-solution is a design I call digital feudalism - of which more later.

If you're interested in joining the Urbit conspiracy, there's a simple step you can take. Take the Nock challenge - that is, write a Nock interpreter, then a Nock decrement formula, and mail them to me. (My Google account is cgyarvin.) While this task is of no use whatsoever, and (as previously noted) decrement is the only formula you will ever write in raw Nock, it makes an excellent pons asinorum. If you succeed, you know your Nock.

In my original post I said that this was "not a difficult problem." This may have been an overstatement. With 16 (unspecified) prizes to distribute, I've received only two (unsolicited) solutions. One of these lucky winners is a math major at Caltech; the other is a math Ph.D in Budapest. So perhaps it is slightly difficult.

But still, you can do it! And now that you know what Nock is for, perhaps you will. He who controls the spice controls the universe...

43 comments:

Matthew said...

Herakleitos would approve.

newt0311 said...

Moving to a more practical subject, may I suggest Google Wave as the starter to Urbit. It is a distributed document update system which seems like it can be worked into a distributed document storage system.

C. Guy Yarvin said...

Google Wave is an extremely fine piece of technology, though I'm not yet clear on its social uses. Also, the operation-rewriting distributed-editing algorithm it uses (I forget the exact terminology), is an excellent example of a difficult protocol to implement. A lot of work seems to have gone into both this and the UI.

However, I would not call GW "distributed," because it has no decentralized or mobile state - at least, that is externally visible. Your Google Wave wave is sitting on a (logical) server somewhere, collecting everyone's wavy little dribbles of thought as generated by their browsers - precisely like any other Web app.

I think GW is best compared to a simpler piece of technology - the revision-control server. This is also in the Urbit ballpark, perhaps closer.

A source-code control system is not exactly a static functional namespace - or, at least, not a very powerful one, because not capable of general-purpose programming. Mercurial is not an application server; Urbit could easily be used as a revision-control server. However, the static namespace is already there and quite useful.

newt0311 said...

Indeed. We need to work on access as well.

Heck, the closest analogue to Urbit right now is probably DNS. If we increase payload size from a few bytes to a few megabytes and then add authentication on top, we would basically have what VJ was talking about in a broadcast system. The biggest problems left then would be the centralized DNS root servers.

Stanislav Datskovskiy said...

Your intended target resembles my own: a globally-unified cache hierarchy.

My aim is for RAM to be purely a cache of disk (in an entirely user/programmer-transparent way) and disk in turn will behave merely as a cache of a global address space. Fetch what you like, read/execute that which you can decrypt.

Distributed Hash Table plus trust metric for the namespace. In fact, abstract over the mechanism for distributed storage, distributed namespace control, and distributed-everything-else with a general-purpose multiparty computation protocol (http://en.wikipedia.org/wiki/Secure_multi-party_computation).

The following will probably sound far more critical than I intend it to. In general, I am a long-time fan of your work - under each of your names.

Algebraic types and immutability: Yuck. Your Haskellian / type-theoretical mis-spent youth is showing. Actual computers contain rewritable storage and will likely always contain it. This is something to be celebrated, not a set of genitalia to be shamefully hidden behind a Christian fig leaf.

http://www.lisperati.com/landoflisp/
Read to the end.

It appears that you have bought into one of the more damaging fallacies peddled by the bureaucrats who replaced computer scientists (as per your excellent essay): that mathematical process can be substituted for genuine understanding, if only we adopt some "hair shirt" paradigm of computation. In reality, there is no substitute for the ability to load a system entirely into one's head and understand it as you might understand arithmetic.

"Jets" are the proverbial "Sufficiently Smart Compiler." The seal between a core of Maxwellian purity and the world of filthy expedient compromises which lies outside must be absolutely perfect - like the seal on the airlock of a multi-generational starship. In fact, building the airlock at all is a terrible idea. Anyone who whines about being welded into the hull doesn't belong on the journey.

Think of every high level language with a C FFI you've used. Having the FFI is not harmless. It colors the programmer's thoughts. It destroys the Master-Of-All-I-Survey majesty of the entire system. Another way must be found. The foundational abstractions must be high-level: http://www.loper-os.org/?p=55

Cutting to the chase: working around the physical limitations of the actual electron-pushing aspect of computation has introduced a flood of ugliness. Your formalism is beautiful, yet it makes no mention of how to prevent a repeat influx of The Ugly. One of us will have to give a (constructive) proof that this is in fact possible.

Right now my bet is on you making it to the finish line first - I started from the (current, artificial) bottom (x86-64) and ended up falling through the floor, mucking about in the underworld of Verilog, clock generators, logic analyzers, and other distractions. And solder rots the brain. On the other hand, a top-down approach risks a Haskellian fate.

C. Guy Yarvin said...

Stanislav,

Thanks for your intelligent comment! You would be amazed at the number of people I've met who have built or imagined something vaguely like this. Urbit is a combination of very well-known ideas, which for some reason I've never seen all together in one place. I encourage you to try the Nock challenge - I suspect you'll enjoy it.

I've also enjoyed a few of your essays. I agree with you that all other software sucks.

I take exception, however, to the inference that any of my misspent youth was misspent on Haskell! I actually do not know Haskell. I also do not know any dialect of Lisp. (I did take one Lisp class, 20 years ago, at Brown- hated it, forgot everything.)

I am actually an OS guy by both training and expertise. And my ignorance of all existing FP systems is intentional, I assure you, rather than indolent. Am I here to praise Caesar? Is FP, to date, a success? You see what I mean.

So when I say "type inference" or the like, all I mean that when I generate Nock from Watt, I first compute

Watt(src) => gene

Mill(type gene) => [type formula]

then can run

Nock(subject formula) =>product

This is the entire formal toolchain. You will see that Mill, the Watt-to-Nock miller, takes a type and a gene, the latter obviously being some kind of AST, and the former being the type of the subject. It produces a type and a formula, the former being the type of the product, and the latter being Nock - ie, "functional assembly language," if you will.

So, if this interface for the Mill function strikes you as inherently mathemolatrous, by all means, continue to assume that I misspent my youth on Haskell! You'll be wrong on both.

In fact, if I had to write "hello, world" in Haskell to avert the death penalty, it would take at least a look at the tutorial. If Haskell supporters admit that Haskell has failed, apologize for inflicting on the world, and agree to at least consider defecting to Urbit, I will apologize for this ignorant attitude. Obviously, a lot of fine work has gone into Haskell. A lot of fine work has gone into a lot of things. It has not necessarily made them fine.

As for jets, yes: they can be screwed up. It is simply taboo to make a system call within a jet. If the OS would let you discard privileges (or has VM instructions that will let you), you could prevent this perfectly and run foreign jets. Otherwise, I would not advise this.

But basically, what you're doing when you write a C jet to accelerate a Watt function: writing your program twice in two different languages. Within a system that is very well-placed to compare the two. If you jet-propel something, it is probably important and should therefore be double-checked. I've found this really quite convenient.

Also, it's not at all the case that you can't write a Maxwellian C interpreter within an Maxwellian functional language, such as Urbit. If you then jet-propel that interpreter, it can be made quite fast. Then, fast machine-level execution requires no other jets - which puts you even farther away from that cursed FFI (foreign-function interface).

Finally, please don't assume that I'm the same person as my good friend Mencius! Some personal blogs pretend to be group blogs. For others, it's just the other way around. Who knows what lurks in the shadows of the Internet? Perhaps it should continue to lurk there...

C. Guy Yarvin said...

newt,

You're quite right - the most important work is protocol work. This comes in two parts: the internal structure of the card itself, and possible networks for routing cards (plus envelope).

For the latter, I think, some kind of hash chording is ideal. Chord networks are very well-known and very resilient. I have no special insights in this area.

The former starts with identity and cryptography, then percolates up into the application layer. Here my designs become rougher and a slight vaporous quality appears.

C. Guy Yarvin said...

Stanislav,

I should add, on rereading your comment, that it's not just that one can write a C interpreter in Watt. Rather, one can write an x86-64 interpreter in Watt (and a C compiler in Watt). A jet implementing the latter has a number of very effective ways to do it - especially given the new virtualization instructions.

At least, if your CPU is an x86-64! And even if this is somehow screwed up, machine-code translation is not *that* bad.

Thus can we mount into the clouds on wings of nouns, yet wallow with the eagles in the biker bar of machine code. We're so abstract, we're actually concrete. The solder reappears.

How does this virtual CPU work? Just take a really king-sized atom, and call it an address space. Take some smaller ones - call them registers. Then, write a step function. If you can't do this and have the result turn out right, the CPU is poorly defined. It probably isn't.

It doesn't matter how impractical your specification of this virtual CPU is - the definition just has to be correct. Such a function will never be run naively except in testing. A virtual CPU will always come with its own custom jet.

Stanislav Datskovskiy said...

C. Guy Yarvin said:

How does this virtual CPU work? Just take a really king-sized atom, and call it an address space. Take some smaller ones - call them registers. Then, write a step function.

I have a suspicion that the entire scheme is vulnerable to Gödelization.

More later. I promise.

newt0311 said...

@Yarvin,

I am not sure a linear chord is the best of technologies. It is too inflexible (for one thing, peers do not decide which documents they are going to archive).

An adaptive algorithm like the routing algorithms we have today seem much more suitable.

A card could simply we a fixed-size immutable chunk of data. Every card "creator" gets a unique 128-bit ID (whose lookup can also be distributed) and can use any of a 128-bit address space for the fixed size immutable cards. These static cards can then be used as the building blocks of a dynamic name-space.

Unknown said...

Ahem. Teaching a cryptography course in Budapest does not make me a CS professor. :-)

P.S. I do know some people who did solve your challenge but didn't bother to submit it to you.

Unknown said...

I still don't like the fact that Nock relies on arbitrary-precision integers and yet cannot do anything with them except for checking for equality and incrementing. This means that real software without jet-power might not even be possible to run once.

I stick by my original proposal: let atoms be bits and let the selector take lists of bits (e.g. nouns like [0 1 1 1] instead of atoms like 14).

This way, raw Nock shall be sufficiently powerful to play with, even if you still need jets to make some things sufficiently fast for whatever purpose. What this means in practice, that for many-many tasks we can skip the tedious work of writing jets; just compile our stuff to raw Nock and run it.

Also, I abhor any idea of digital feudalism. One Verisign is already too much. There is a better solution to Zooko's triangle:

Cryptographic hash suffixes: the identifiers are long (e.g. 256-bit) numbers, BUT you are allowed to use any suffix thereof assuming the security risks that come from that. In practice, 64 bit suffixes will almost always do and they are:

1. Not much more taxing on the human brain than telephone numbers.
2. Sufficiently secure against casual pre-image attacks.
3. Sufficiently unique for large numbers of named entities.

C. Guy Yarvin said...

I still don't like the fact that Nock relies on arbitrary-precision integers and yet cannot do anything with them except for checking for equality and incrementing. This means that real software without jet-power might not even be possible to run once.

Correct - real software without jet-power is not even possible to run once. I don't see how restricting atoms to 0 and 1 would help with this! Alas, real software with a 1-page interpreter will probably always be a pipe dream.

The question is whether you trust your jets. Once you trust your jets, you start forgetting that they're there. Logically, they're not. But do you trust your jets?

Indeed, a bad jet can really screw you up. The worst failure mode is one in which the Nock formula is *not* working as intended, but the C code *is*. When this happens you start drifting away from Maxwellian computing, very fast.

To avoid this horror, my interpreter has not a jet-propulsion switch but a jet-propulsion knob. So at -O0, you are running pure Nock. At -O1, dec is jet-propelled, but add isn't. At -O14, parsing is jet-propelled. And so on.

C. Guy Yarvin said...

P.S. I do know some people who did solve your challenge but didn't bother to submit it to you.

Fortunately, they're not too late!

newt0311 said...

@Yarvin and Daniel

It seems like jets are an indication of a fundamental problems with Nock. Nock does not reflect the underlying reality of the machine.

Either use something that is closer to assembly (and therefore may be slightly impure but at least doesn't need to be tainted by jets) or redesign the machine to evaluate Nock effectively.

Right now, you are writing the program (any program) twice effectively. Yes, this is only in the compiler but that is just like using a library. The first time, written in the pure Nock fashion is not even used and the second time, which is used is "impure" so whatever benefit Nock provided is lost. Without a guaranteed means of verifying the equivalence of the two blobs of code, Nock is just a very expensive waste of time.

C. Guy Yarvin said...

Also, I abhor any idea of digital feudalism. One Verisign is already too much.

But two Verisigns would be better than one, n'est ce pas?

I agree that there's something terribly wrong with the Verisign model. If you can conceptualize what's wrong with it, it might help you consider alternatives.

In practice, 64 bit suffixes will almost always do

I would say that cryptographically, 128-bit suffixes will almost always do. 64 makes me nervous, as does the word "casual." But hey, you're the crypto man.

The problem is: 64 isn't good enough. From the user perspective. From the user perspective, you really start cooking with gas when you get down to 32. Fingerprint suffixes will no longer do.

So the solution is: both. Identities above 2^64 are 128-bit hash suffixes ("wild"). Identities below 2^64 are assigned feudally ("civil").

Urbit has both its city and its barbarians. The existence of wild identities helps keep the civil sphere honest - ie, if it degenerates into a digital despotism, everyone who wants to remain free just has to remember longer names. Of course, there are a number of other safeguards...

Stanislav Datskovskiy said...

newt0311 said:

or redesign the machine to evaluate Nock effectively.

I'm about to try implementing a Nock processor in an FPGA. This promises to be entertaining.

newt0311 said...

@Stanislav

It will be. How do you plan on handling memory management?

C. Guy Yarvin said...

newt,

The jet isn't really "impure" in the functional sense, because it doesn't have side effects. In fact, it needs no OS privileges - just a block of memory.

Yes, you are writing your function twice! I have done quite a bit of this, so I can speak to the experience. The result is (a) not twice as much work, and (b) much more than twice as reliable.

Moreover, you don't have to do this in ordinary programming. You have to do this where, in a non-Maxwellian environment, you'd just write a native method. Even Java would probably be improved if all native methods (that were native only for speed, not for system calls) had to come with a parallel specification in pure Java.

Nock is actually not that hard to compile to machine code, I think. At least, relative to other languages in its class. However, this is a significant engineering project which I'd rather not have in the critical path. Slow interpreters with optimized library routines are well-known to be viable...

C. Guy Yarvin said...

Without a guaranteed means of verifying the equivalence of the two blobs of code, Nock is just a very expensive waste of time.

Well, a guaranteed means is a lot to ask for! Mathematically, I mean. However, if you dial optimization down and run the Nock formula, the jet still runs. And its result is compared to the formula's result.

So if ya want verification - that's a research project. However, if you can be content with mere testing, this process will test your code quite unobtrusively and effectively.

newt0311 said...

@Yarvin

The jet isn't really "impure" in the functional sense, because it doesn't have side effects. In fact, it needs no OS privileges - just a block of memory.

Without a new OS (and even with perhaps), the above simply cannot be verified. Unless you are the only one writing jets, your solution is unsatisfactory.

Even Java would probably be improved if all native methods (that were native only for speed, not for system calls) had to come with a parallel specification in pure Java.

Believe me when I say that Java does not have many of these. Most Java methods which do not need system calls are in Java. However, the reason they can do this is because JVM bytecode can be run efficiently on x86 computers.

Nock is actually not that hard to compile to machine code, I think. At least, relative to other languages in its class.

The entire class is nearly impossible to work with. Even GHC takes a few short-cuts from pure lambda calculus and whether you like it or not, GHC is the closest that you are looking at here.

Slow interpreters with optimized library routines are well-known to be viable...

Interpreters can not run themselves like compilers can compile themselves.

However, if you can be content with mere testing, this process will test your code quite unobtrusively and effectively.

If testing is all that Nock gives, it is a worthless idea. Testing can be done quite well without Nock. Everybody knows what they want their program to do. The problem is making sure that the program actually does it. Testing is what everybody does today and clearly (according to you), it is not sufficient.

Example: If you want to jet a parser, the testing better have damn good coverage. Far better to have an automated system of parser generation and then be able to define a parser in a few lines.

In an earlier post:I would say that cryptographically, 128-bit suffixes will almost always do.

Famous last words.

Actually, from the user perspective, anything in terms of bits is too much. Notice now that nobody remembers a slew of phone numbers. They remember a bunch of names (sometimes) and use a mapping to go back and forth. The same applies to the internet.

The same solution is needed for Urbit (that is why I wanted to use Urbit as the base layer and build a dynamic file system on top). Assign identifiers with whatever number of bits you want (enough so that we don't run out) and then make a mapper back and forth. Digital feudalism will work quite well here as it has worked for DNS and IP addresses (which are pretty much exactly the same problems -- uniquely naming entities). If people want a strong identity match, they will have to contact the entity and get some keys themselves. This can be done through the web of security that VJ talked about. In practice, I think that this will be almost equivalent to the digital feudalism idea (unless I am misunderstanding your digital feudalism idea which is quite possible) but slightly better because there is some verification.

Stanislav Datskovskiy said...

newt0311 said:

How do you plan on handling memory management?

For now, something like the usual cons cells (like the SCHEME79 chip.)

newt0311 said...

@Stanislav

Good luck.

C. Guy Yarvin said...

Example: If you want to jet a parser, the testing better have damn good coverage. Far better to have an automated system of parser generation and then be able to define a parser in a few lines.

By "parser" I actually mean "metaparser," ie, a function whose arguments are a text file and a constructive grammar. So, yes. It's this that gets the jet. It's not your grammar that gets the jet, because the typical formula in the grammar is just doing some consing.

Everybody knows what they want their program to do. The problem is making sure that the program actually does it.

Well, what you're testing is that two programs are equivalent. You could have written the same bug twice - but that's a lot more unlikely.

There are two ways to test: with two programs, and with one program and a bunch of hand-checked test cases. I prefer the former.

Actually, from the user perspective, anything in terms of bits is too much. Notice now that nobody remembers a slew of phone numbers. They remember a bunch of names (sometimes) and use a mapping to go back and forth. The same applies to the internet.

Consider the way Facebook does it. There are three Facebook identities: the ID, a number that appears to be about 32 bits; the real name, which is not unique; and the username or handle, which is unique and first-come first-served.

The Facebook ID is not memorable, as such. However, it's straightforward to write a function which invertibly maps a 32-bit number to a string which *is* memorable. I've done this. The function could probably be improved, but here are some random examples:

176.215.16.104 == "divzip-dibbel"
30.122.0.74 == "pobmol-dabmek"
149.229.247.52 == "nitvas-siztif"

Not exactly high technology. But you'll see that the latter is a lot more memorable than the former - not as memorable as a human name, of course, but not too far from a classic handle such as "monkey79." And unlike either, it does not require a central directory.

Now, on top of this namespace, you'd certainly want to maintain a *real* namespace that would bind human names to these entities. There's no substitute for human names. However, if you have a numeric identity which is significantly more memorable than, say, phone numbers, you have a simple, solid layer on which to build a human name directory at a higher level.

Human names are the most memorable. But managing human names, both individual and corporate, is a huge business problem. If you have a lower-level identity system which is usable, clean and simple, you have a good substrate on which to build the higher-level names.

This is why Facebook started with IDs and built human names above it, then added usernames. My guess is that if Facebook could make IDs more memorable in this trivial way, usernames would not be needed.

But, of course, Facebook IDs make you basically a serf of Facebook. No one should have to be a digital serf...

C. Guy Yarvin said...

Stanislav,

I'll second that - FPGA nock would be mondo cool. Of course eventually it will need FPGA jets, as well. Unfortunately, my hardware chops are almost nil, so I really have no other advice! Still, the beauty of a small spec is that it needs no guru...

newt0311 said...

@Yarvin

There are two ways to test: with two programs, and with one program and a bunch of hand-checked test cases. I prefer the former.

Then why bother with Nock? It is quite possible (and easy) to make a human understandable language with easy semantics -- scheme being one possible example. Then the scheme version can be tested. Of course, there is an even better solution -- the scheme version can be compiled and testing is not necessary. Mathematical equivalence in that is case is indeed guaranteed by the compiler.

As to your "memorable" 32-bit numbers. They don't seem to help. Also, the routing framework which helps to find the number is much more an overlord than the name-resolution system. If somebidy is really so worried about the naming system, they can come up with their own registry as a person can now (try to) do with IP addresses and bookmarks.

Unknown said...

Two Verisigns are not viable: the second will be bought up by the first in short order, because one is more profitable than two. Hence Thawte's acquisition.

But why not use suffixes (or prefixes) of wild names and let people decide how long a suffix they want to use? PGP got it right with the fingerprint (160 bits), the long ID (64 bits) and the short ID (32 bits). Yes, I can generate a key that matches anybody's short ID, but they can always fall back to using longer IDs, so I won't bother attacking even 32-bit names, but they can (and do) collide by accident as well. Now, 64-bit ID's are substantially more difficult to attack (requires huge botnets or specialized hardware), and they do not collide by accident. And still, you can always fall back to the fingerprint.

Now, this same idea can be generalized by letting people use arbitrarily long suffixes (or prefixes) of their wild names. Spanish aristocrats have done so quite successfully. Also, for most students of cryptography Al-Kindi means Abū Yūsuf Yaʻqūb ibn Isḥāq al-Kindī even though there have been quite a few Al-Kindi's out there.

Unknown said...

I like the knob idea, but the problem with Nock is that you cannot fully turn the knob to raw Nock, because it won't execute once in the programmer's lifetime. Hence my suggestion with binary atoms.

C. Guy Yarvin said...

I'm not a PGP geek, and I've never seen either a 32-bit, or I think a 64-bit suffix, in the wild. I didn't even know they existed. Thank you for explaining them - I now know how they work, too.

In the PGP context, these short IDs are pretty cool. In the Urbit world, they don't really work, and here's why.

The trouble with this approach is that the suffix is (in many cases) enough for verification of an identity that is already communicated through another channel. But it is not enough to serve as the root of a namespace.

If you can say "/id/file," id needs to be unambiguous - not only can collisions be attacked, but even resolution becomes very problematic.

C. Guy Yarvin said...

I like the knob idea, but the problem with Nock is that you cannot fully turn the knob to raw Nock, because it won't execute once in the programmer's lifetime.

Sure you can - this is a stateless system, after all. It doesn't have to boot. You can't process packets and resolve names, but you can turn the knob to raw Nock and test add, multiply, etc.

There's also a lot of opportunities for metacircularity in this system. Nothing stops you from writing a raw Nock interpreter within a jet-propelled Nock environment.

(Normally even metacircularity will be accelerated, though. For example, one thing I think we'll see at the Urbit level is Nock with an extra operator 7 - dereference Urbit path.)

newt0311 said...

@Daniel

The User IDs are not designed to be a security measure (at least not anymore). The cryptographic (and nearly impossible to fake) hash signatures are. If you rely on the 32 or 64 bit IDs for validating keys, you have a problem.

@Yarvin

Why mix identification and validation?

Any organization has a unique ID and a certificate with lots of identifying information and a cryptographically secure signed hash liking the organization to the ID. There is no need for there to be a link between the keys an organization uses and the ID it has. IMO, such a link is a terrible idea. What happens when an organization wants to revoke a key but not its ID or vice versa?

What is the point in creating this useless link?

Also, I think my last comment was approaching the heart of my problem with Nock: what is the purpose? Yeah you find it aesthetically pleasing but so what? Nock isn't useful to program in because it is too low level. It is not useful as an IR because it is too far from machine language. It exists in limbo as a marginally interesting CS project. VJ's idea of broadcast documents is very much possible without Nock. Heck, it is quite doable in our current ecosystem of URIs and protocols (modulo network externalities).

Unknown said...

@newt: But we are talking about references here. Also, you can safely rely on 64-bit IDs for validating keys as long as the value that you are protecting is less than the cost of the attack, which is actually quite often the case. As long as it is the user's choice, it's not a problem.

For example, suppose that weather forecasts are signed with some key. I am perfectly content with referring to that key by its 32-bit ID, because there is very little risk involved on my part. Other people, who rely on those weather forecasts for some economic activity, might be more cautious as to what they accept, so they might go up with the bit count.

newt0311 said...

@Daniel

If that is all you need, use X.509 certs. They are relatively easy to get -- only a few dollars per year (which for an organization is a pittance) and the risk from a central authority is far far lower than the risk of forgery from a 32 or 64-bit ID.

PGP is quite capable of using X.509 certs seamlessly.

If you have a friend, then exchanging verified certs should be easy and you can sign the certs yourself.

Unknown said...

@newt: That's absolutely unacceptable. Actually any amount of money is unacceptable for identifiers.

C. Guy Yarvin said...

For example, suppose that weather forecasts are signed with some key. I am perfectly content with referring to that key by its 32-bit ID, because there is very little risk involved on my part.

Exactly. The trouble is that this works when you're trying to validate a weather forecast that you've referenced by other means. When you're trying to find the data from the name, however - dereferencing /ID/weather - teh ugly emerges.

VJ's idea of broadcast documents is very much possible without Nock.

Yes, it is! However, if you're trying to standardize a *functional* rather than a simply passive namespace, you need to standardize functions. This is the purpose of Nock, in two words: standardizing functions.

As for Nock as an IR, this will be a lot clearer once you can see and play with Watt. IR is a very general term. Nock should not be confused with RTL, but it is definitely intermediate and it's definitely a representation.

C. Guy Yarvin said...

Two Verisigns are not viable: the second will be bought up by the first in short order, because one is more profitable than two. Hence Thawte's acquisition.

I missed this comment and need to respond to it.

What's unacceptable (to me) is monopoly or near-monopoly ownership of a namespace. I'm not opposed to paying for identifiers, because any sort of short identifier experiences contention in a successful system; that contention needs to be resolved; it can only be resolved economically.

Moreover, not only is there no real contention for wild identities, there is even no real contention for 48-bit identities. Contention only begins at 32 - and it only begins once the system is quite successful. For the foreseeable future, even short identities are free (as in beer).

So: let me answer your question. If you have two, the pressure to amalgamate is great, because one has monopoly power. If you have, say, 255, however -

Small amalgamations do not confer any monopoly power. To become Verisign, you need *all* 255. This is quite difficult to acquire, especially if the 255 are distributed widely and among holders with benign (ie, non-mercenary) ulterior motives.

Such as EFF. If EFF had had Thawte's rootkey, would it have sold out? Highly doubtful. The trouble with browser rootkeys is that the system evolved in a ridiculously ad-hoc manner - nobody was actually trying to design a stable oligarchical regime that would not collapse into a monarchy.

Not that monarchy is the end of the world. But oligarchy is far more desirable from the user's point of view. And since there is contention, anarchy is not an option - someone has to rule.

newt0311 said...

@Yarvin

Yes, it is! However, if you're trying to standardize a *functional* rather than a simply passive namespace, you need to standardize functions. This is the purpose of Nock, in two words: standardizing functions.

Except, there is nothing about Urbit that is defined in terms of what it does internally. All we need to know it that Urbit, somehow implemented, when given a card and a deck returns some information and that upon addition to the deck, still returns the same information. How the urbit function goes about doing this seems rather irrelevant. You yourself said that how a computer acts is up to itself. As for the "deck", it seems better seen as a massive bitstream that we lesser mortals like to call "software" and "the internet." We need know no more.

C. Guy Yarvin said...

It's quite essential what the function is - if you want to move your deck from one hosting service to another! After all, it's not really a proper migration if it doesn't mean the same thing in the new place as the old.

You'll observe that standardized, general-purpose hosting is one thing a lot of people want, but none of them seem to have...

newt0311 said...

@Yarvin

Then what exactly is AWS, Rackspace, etc...?

We do have a standardized functional language -- x86 and x86_64.

C. Guy Yarvin said...

Sorry - the word I was looking for was "portable."

Have you ever called AWS and asked them if they could port your image over to Rackspace? If the answer is "no," ask to speak to the manager. :-)

Moreover, an x86-64 virtual server in the sky, even if AMI or some other virtual image format could be standardized, is about the most cumbersome and unmanageable thing in the world. The difference between it and Urbit is like the difference between a tank and a car. "Let them drive tanks" is not a valid objection to my plan to build cars!

newt0311 said...

@Yarvin,

Have you ever called AWS and asked them if they could port your image over to Rackspace? If the answer is "no," ask to speak to the manager. :-)

Good point. However, that seems like a problem that will be fixed in time.

Moreover, an x86-64 virtual server in the sky, even if AMI or some other virtual image format could be standardized, is about the most cumbersome and unmanageable thing in the world.

First off, AMIs are already standardized. You can even download them off of S3 if you are interested. Its a self-contained (efficient?) compressed set of files which tell Amazon systems everything needed to run an instance. AFAIK Amazon uses Xen which is sufficiently standardized to be available to anybody who runs linux.

The probable (to me) reason we don't have a standard format for machine images is that the market simply isn't large enough for this.

Also, do you have any guarantee or argument whatsoever for asserting that Nock decks will not be similarly cumbersome? Nock code is certainly more cumbersome than ASM and machine code which doesn't bode well.

C. Guy Yarvin said...

I agree that something like AMI can be standardized. However, this is simply not a *consumer* interface to the cloud. It is an industrial-computing interface.

AMI obviously does not standardize any higher protocol or application layers. The problem of how you port your AWS account to Rackspace is a solvable problem with present approaches. The problem of how you port your MySpace account to Facebook, or your Yahoo account to Google, or whatever, is not.

This is what I mean by "a tank, not a car." I hope it clarifies the matter...

newt0311 said...

@Yarvin,

A functional namespace is not needed to move a facebook account to MySpace. A file namespace seems sufficient.

Are you thinking of something along the likes of Google's Django hosting solution?