Lambda the Ultimate

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?