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