Urbit: Functional programming from scratch

C. Guy Yarvin recently published an interesting new project in language/systems design. It includes a simple formal model of computation called Nock ("comparable to the lambda calculus, but meant as foundational system software rather than foundational metamathe­matics") and a self-hosted language called Watt that compiles to Nock. The motivation? To provide a fully-specified foundation for Urbit, a hypothetical system architecture that uses content-centric networking to distribute code and data in a functional global namespace.

Yarvin's own descriptions are rather lengthy, so I tried to provide a shorter introduction here.

Interesting questions for LtU readers: Nock formulas are terribly inefficient for real computation (for example, decrement(n) is an O(n) operation). Yarvin intends to make Watt efficient by writing fast implementations (in C, say) for standard "kernel" functions like decrement, add, multiply, and more. He calls these fast native implementations "jets." So how one can trust that jets are equivalent to the functional Nock/Watt code that they replace? Yarvin has proposed the classic n-version software engineering trick of comparing both implementations with the same inputs, but in addition the classic problems with that approach, there is the additional hurdle that the pure Nock code might be so inefficient that it is impractical to run it on most inputs. Is the goal of a minimal pure standard compromised by the need to implement a common set of "impure" jets too?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Not to knock nock

... but why not just use lambda calculus or some combinator calculus? How much simpler than LC could this possibly be? Nock is an impenetrable language serving to formally specify programs, but there's no accompanying formal logic for proving the translations to real code equivalent? Huh? I must be missing the point.

In particular...

Why not lambda?

Indeed, the SK calculus is even simpler to specify than Nock. (The normal lambda calculus with variables and alpha-renaming and such is not; Nock is much closer in simplicity to Brainfuck than LC.)

Perhaps Yarvin created his own low-level language partly out of desire for a clean break. But maybe he also believes the total complexity of Nock plus a Watt compiler will be less than the total size of, say, SK plus a similarly expressive high-level language compiler.

[edit: oops, this was supposed to be a reply in the thread above]


Nock reminds me of SK more than anything else.
Specifically, of Unlambda, the most purely SK-based language I know of.

I found myself brushing up on SK when solving the decrement-puzzle.