Of Decaying Urbits.

After the sale of my Urbit ‘dukedom’, several readers have written to me, asking ‘why.’ The following was my reply to one such letter, from a fellow who suggested implementing a proper hardware foundation for Nock (Urbit’s computational base.)


Dear [Reader],

Here was my own Nock.

But notice that I made no attempt to implement a Nock in FPGA. To understand why, I recommend: trying it yourself!

I confess that I am entirely uninterested in any further doings involving Nock. To learn why, read on…

The proof of the pudding – if you will – or of the turd, if you must! – is in the eating.

It isn’t that one could not, in principle, wangle together some silicon which executes Nock. But the impedance mismatch between any physically-plausible machine and anything resembling Nock is atrocious. And I do believe that this actually matters (further discussion here.)

The whole concept of ‘immutable data’ (and the more general idea of a formula-reduction approach to computation) is a fundamental dead-end. This is because physical machinery inescapably relies on mutable storage – and the reasonably-efficient use thereof.

The approach taken by Curtis is a result of his mis-spent youth among academics, who accept the costs of this ‘hair shirt’ approach to computation because it allows them to write ‘proofs’ (not to be confused with actual mathematical proofs. The very notion of proving any important property of a computational system as a whole, rather than of an abstract algorithm taken individually, is laughable – because real-world situations do not give you the kind of hard priors required to rise to the level of an honest mathematical proof.)

A. Perlis taught that ‘one cannot transition from the informal to the formal by formal means.’ And indeed you can’t.

The ‘proofs’ so beloved by FP academics are written in order to participate in a bizarre grant embezzlement scheme, rather than for any practical purpose. They are fruits of a poison tree, just the same as anything created by Lysenkoist biologists.

Curtis himself meditated on this fact back in ‘07, but has proceeded to give us exactly the kind of thing he condemned.

Likewise:

‘This is also the reason why functional programming languages ignore macros. The people behind them are not interested in programming automation. Wadler created ML to help automate proofs. The Haskell gang is primarily interested in advancing applied type theory.’ (Vlad Sedach, quoted in ‘Of Lisp Macros and Washing Machines’.)

The people who gave us the pseudo-mathematical ‘computational astrology’ on which Nock is ultimately based did not have the best interests of your brain in mind! Quite the opposite, in fact. Their one and only objective was to make themselves seem clever while adding to a titanic pile of drivel, beneath which virtually all honest work in computer science was mercilessly crushed.

Curtis answered the inescapable clunkiness of formula-reduction with ‘jets.’ And even if the latter did not rely on efficient solutions to NP-hard problems (formula recognition), they are a total cop-out from the ‘turtles all the way down’ approach we’ve been promised. The result is fundamentally rotten.

Anyone who steps up to the task of re-creating computing from the ground up must take hold of the entire stack – software and hardware – and fit it in his head as a coherent whole. This is the only way to reduce the moving parts to an absolutely-essential crystalline minimum. Urbit is quite clearly not the result of such an undertaking. Curtis baited our appetites with the promise of a ‘Year Zero’, and instead gave us a craven surrender to Unix and the von Neumann machine, with yet another layer of even less-comprehensible crud plastered on top.

‘Proof,’ especially of the pseudo-mathematical variety, will never substitute for: understanding. The kind of understanding you have of arithmetic, or of a doorknob. (Where is the mathematical proof that your doorknob turns? And yet it turns!)

It is possible to build a computer which an educated person can understand – in exactly the same way that a Pashtun blacksmith understands a Kalashnikov. But in order to actually do this, one must first believe that such a thing is possible.

Like the infamous Galloping Gertie bridge at Tacoma Narrows, Urbit is now and will forever remain of great educational importance – to all would-be cleaners of the Augean Stables of modern computing. As an elaborately-worked example of what not to do!

If you are interested in physically-plausible and effective bottom-up redesigns of the computational stack, study the Scheme-79 chip and related work. Or better still, consider what can be built from the asynchronous Muller C-gate, and how well the latter plays with a pure-dataflow computational paradigm.

Yours,
-Stanislav

This entry was written by Stanislav , posted on Saturday December 21 2013 , filed under Computation, Distractions, Mathematics, NonLoper, Philosophy, SoftwareSucks . Bookmark the permalink . Post a comment below or leave a trackback: Trackback URL.

17 Responses to “Of Decaying Urbits.”

  • ginko417 says:

    To be publicly critical of a project that is still so young and involves so many degrees of freedom reflects poorly on your own intelligence.

    • Stanislav says:

      Dear ginko,

      The “degrees of freedom” you see are illusory. Where is the freedom to abandon the moronic formulae-reduction paradigm? Immutability? Are “jets” to go away, and if so, how? If you came here to have an actual scientific conversation, I’m all ears.

      It is said that Queen Victoria once asked Michael Faraday: “Of what use is electricity?” To which the great man replied: “Of what use is a baby?”

      But in the case of Urbit, we have a: hydrocephalic baby. This little fellow will not be growing up to be an astronaut.

      The entire thesis of this blog is that foundations matter. That you cannot “get from here to there” for arbitrary values of “here” and “there.” That you cannot get to the moon by piling up chairs. Or to a sane paradigm of computing from Unix and the von Neumann fossil – or from the detritus of 1990s American academia.

      And if you are one of the many people who disagree, and believe that anything can be readily turned into anything else with sufficient sweat, there is a whole world of busy bees ready to welcome you into their hipster hive – where you can merrily pass the time attempting to stitch sow ears into silk purses.

      If you are this kind of busy bee, Curtis needs you! Last I heard, he is still struggling to come up with a memory allocator that doesn’t bomb when the moon is in the wrong phase. But this little oasis does not belong to your kind. Contemplate your pyramids elsewhere. Get out and stay out.

      Yours,
      -Stanislav

      • I still hate commenting on loper because of the captcha system, but anyway :

        Dear ginko,

        A) the project is not young ;
        B) not being critical of the idiocy of the young is how you got to be old and stupid in the first place. Yes, yes, you’re not stupid, you’re a splendidly excellent&remarkable snowflake of unique brilliance and I’m an evil nonperson that calls random people he never met (and would love if he actually did meet – especially your great sense of humor, and the way you respect a girl woman!) stupid wantonly. Sure.
        C) Judging other’s intelligence on the basis of the very little you understood of the very little you read of what’s going on reflects greatly on your economic value.

        Hugs and kisses,
        etc.

  • ginko417 says:

    Dear Stanislav,

    Your general premise that “foundations are important” is non-controversial. Perhaps this is the reason why the Urbit project is so exciting — fixed number of addresses (solves problem of spam), full encryption (solves problem of privacy), etc.

    The fact that the project has been merged into a corporate structure does not concern me; a tightly-knit core development team, corporate structure, and decentralized version control via Git is a proven model of delivering innovative software projects.

    Can you please summarize why each of the items you have flagged represent “fatal flaws” — i.e. formulae-reduction, immutability, and jets? This further explanation would be valuable for the rest of us who are independently evaluating probability of success.

    • St Gregory of Nyssa says:

      Until the software Stannis responds himself, here are some things that I’ve disliked:

      1. Immutability is fundamentally untransparent because the machine itself is mutable. It obscures your understanding of what is going on inside the hardware rather than helping it. Many programs are also more intuitive when you write them with mutable functions.

      2. The Nock foundation obscures meaning. Decrement isn’t a basic operation and requires linear rather than constant time. This is unacceptable for a lowest foundation which you can expect a person to use and understand.

      3. Urbit gets around the problem of inefficient representation by using jets, which means bringing in code that is closed source, uninspectable, and undebuggable. This prevents you once again from understanding the computation and testing subcomponents within the jet.

      • Stanislav says:

        Dear St Gregory of Nyssa,

        1-3: I couldn’t have explained it any better myself.

        Only thing is: now you must tell us which character from G.O.T. Curtis is!

        Yours,
        -Stanislav

      • Dave says:

        Stanislav,

        You criticize Mr. Yarvin for choosing to rely on “jets” – which apparently are black boxes of hidden complexity and unpredictable run-time optimization.

        Yet, you highlight the Schem-79 paper’s description of an unpredictable run-time optimization of the stack as an example of something worthy of aspiration.

        I’m not a systems guy – just a regular DSP engineer. Am I misunderstanding something? I realize one is hardware and one is software – but is that the only basis for the objection to jets? Or is it because they rely on several layers of hidden complexity?

    • Jakub L says:

      Dear ginko,

      if I may be so bold:

      In my view, the things you mention (and many more, like strong typing) are fundamentally wrong because they straightjacket the operator into a given way of thinking. The system has to give you freedom to do anything, not lock some options away because they were anti-doctrinal in the eyes of some FP bozo.

      Not to mention that colossal fragmentation of principles abounds when the initial hype wears off and people realize that they actually have to do things like I/O (Haskell, where monads and switching back to the good ol’ imperative paradigm are an absolute must for your program to be able do anything even remotely useful) or build data structures quickly (Clojure and its clojure.lang.TransientWhatever, which could have merrily be part of clojure.lang.PersistentWhatever if only the designer was able to think for himself and wasn’t sporting the eye blinders of modern FP hype).

  • tudo says:

    Dear Stanislav,

    I wish you could explain these things with more details (or having some link to explain the concept):

    – Can you give a more concrete example of the difference between proof in mathematics and “proof” in FP?
    – What are jets and formula-reduction in FP? Is the formula-reduction different compared to Math?

    Thanks.

    • Stanislav says:

      Dear tudo,

      Here is a brief example illustrating the difference in question:

      1) An FP academic writes an elaborate proof, with plenty of squiggly marks and Haskellian hair-shirt arcana, regarding the impenetrability of a security mechanism.

      2) Dr. Evil, having obtained an unprivileged account, executes an undocumented Intel instruction, goes straight to ‘ring -1′, and gets root on the box anyway.

      The mathematical proof was technically correct, but its author did not have a solid handle on the priors. This is because he was dealing with a physical machine, rather than the formal system claimed.

      Formula-reduction is a perfectly-valid mathematical formalism. It simply doesn’t map directly to any kind of machine one might physically construct. Hence ‘jets’ – a non-mathematical cop-out, where a system operating at a lower and unspecified level of abstraction is supposed to recognize operations which cannot be efficiently represented in Nock, and carry them out via some other means.

      The best way to understand what Curtis actually did is: to read his code. Which I have been doing, on and off, since he placed it in a public repo, several years ago. Don’t take my word for it! read what he wrote.

      Yours,
      -Stanislav

  • ginko417 says:

    St Gregory,

    Thanks for your response, while I appreciate your distaste for some of the design decisions, I am not sure I see any “fatal flaws” here.

    1. Just because hardware is mutable doesn’t mean that an attempt to make data immutable is a “fatal flaw”. To me this looks more like a “foundational decision” that will lead to new kinds of benefits and limitations in terms of performance, usage, and programming, wholly unique from anything we currently know or understand – but not sure you can “prove” it is a dead-end?

    2. On the point about “Nock foundation obscuring meaning” — don’t all natural and formal languages have this problem to a certain extent? How is this a “fatal flaw”? Its like saying that English language is fatally flawed because it lacks nouns to describe 50+ varieties of rain and snow, which is something the Inuit languages can do.

    3. Using jets today looks like a “quick fix” to something that isn’t fully evolved yet, but makes stuff work “well enough” that other parts of the project can continue to advance. You have to be pretty unimaginative not to foresee additional layers of definition, precision, and functionality evolving on top of Nock to address where jets are being used.

    Unless Stanislav can demonstrate how any of these things are “fatal flaws”, I’m going to interpret his decision to sell his Dukedom and publicly bash the project as follows:
    – CY has been a bit arrogant with design decisions,
    – Stanislav who has added a lot of value to the project and is feeling increasingly disrespected, and
    – with a competing project in the wings Stanislav has personal incentive to undercut CY’s initiative

    regards, Ginko

  • Luke McCarthy says:

    Urbit is peculiarly obscurantist and uses unnecessarily nonstandard terminology. That’s enough to put me off.

    • Dave says:

      Urbit is peculiarly obscurantist and uses unnecessarily nonstandard terminology. Agreed. Curtis claimed to create the “C” of Urbit programming, but Hoon strikes me as the PL incarnation of an anti-reserved-keyword-zealot’s rant.

  • mnemnion says:

    Dear Stanislav,

    Thank you for your reply.

    It may be the case that you, Curtis and I simply have subtly different goals. Suggesting that the sum may prove greater, if we can achieve a mutual understanding.

    May I strongly encourage you to work out a coherent post on the potential of the Muller C-gate for general computation? I get the same tingly spidey-sense from that circuit that I get from discussions of memristance: it’s clearly important, and there’s no modern, clear-minded exploration of how one might compose it into units of computation.

    Metaphor is powerful stuff! You’re searching for a solid bedrock abstraction, one that reaches down into the hardware. More power to you; as I indicated elsewhere, I’d happily pick up the same model FPGA dev board you’ve been using, just to run your code.

    Curtis is not interested in bedrock. What use is bedrock to a naval fleet? It is a place to drydock ships that aren’t working. Urbit floats upon the C! This is a choice, not a cop-out. There is an enormous ocean of C, and barely an island of sensible rock to be found, although Chuck Moore is selling real estate.

    I find bedrock to be fascinating, crucial, and hard to find in the wild. In the wild, however, I could write a whole virtual reality in C# and OpenGL. I can buy arcane objects of ridiculous latent power, like the BeagleBone and the Parallela.

    The challenge is one of domestication. Do cellular automata, and formula reduction, have anything to offer here?

    Perhaps. The promise is composability. Ax differs from Nock on a few key points, such as providing ordinary arithmetic. More importantly, it provides paired operators, `put` and `branch 0`, which provide formal mechanisms for input and output into a running arc of Ax code. Ax arcs are themselves composable into larger structures: Hermetically sealed, with ports to attach plumbing.

    Nock is far more all-encompassing, which may prove to be a mistake. It certainly requires more cheating. To which, two points: One is that a certain amount of cheating is encouraged when you’re rewriting strings. There are genuine advantages to powerful mathematical formalism. The second point is that the motherships are still leaking memory. We may hope the transition to the LLVM helps in that department: I reckon that tar and oakum will suffice, for now.

    Using Ax, a ‘jet’ is a conceptually clean thing: we ask the underlying architecture for a number, then we get that number. There is no pretending that we did a calculation that we did not; no need, we have a way of exporting a noun from a running process and a way to import same.

    Urbit is immediate and social, and I wish them luck. I’m impressed enough with the whole shebang to give Hoon exactly one more shot, when the ‘runes’ are fully documented.

    The tool I lack is an encounter suite. I look at the landscape of our current hardware and see shackles imposed by ignorance. The open source community is utterly failing to penetrate into device drivers and firmware, because we haven’t built the tools to wrestle hostile hardware into submission.

    I eagerly await your fortress of Lisp, Loper. I am perfectly serious. Give me a keyboard, monitor, and an FPGA, write a system where Scheme is the only turtle, and I will use it as soon as the board arrives. A Fortress of Solitude, yes, but magnificent, fully worthy to stage a colonization of the world at large.

    In the meantime, and always, we have hundreds of existing computers per human, produced via the most energy intensive activity per gramme that the world has ever known. Let’s not waste a substantial fraction of human toil, just because the output is sub par! Can our existing boards be transmuted into tools for conviviality? I have faith.

    I am aware of only one way to REPL hardware, and that is the way of Forth. Forth is abandoned in open software; one may hear the wind blow through the corridors. Weirdly, everything was written in the 90s, last edited around 03, and works fairly well. This is a good sign.

    I count roughly eight important computers on my phone, being conservative about what constitutes a computer. Safety for civic society absolutely requires that we tame those beasts, which are hiding behind opacity simply because we lack the most basic tools for interactively deriving their function.

    Rather than throw another thousand words at tying this braid together, I will leave it a mess of loose ends. Ultimately, in our game, code speaks.

  • name redacted says:

    Revised Report on the Propagator Model
    Alexey Radul and Gerald Jay Sussman

    “The Propagator Programming Model is built on the idea that the basic computational elements are autonomous machines interconnected by shared cells through which they communicate. Each machine continuously examines the cells it is interested in, and adds information to some based on computations it can make from information from the others.”

    • Stanislav says:

      Dear name redacted,

      This model also made an appearance in Abelson & Sussman’s well-known SICP.

      Unfortunately, it is a high-level (Scheme) model – rather than a physical machine. Quite a bit of fun to play with, but it does not teach us how to construct the machine.

      Yours,
      -Stanislav

Leave a Reply

XHTML: You can use these tags: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong> <pre lang="" line="" escaped="" highlight="">