Urbit: A clean-slate functional OS

Let me bury that criticism though by saying that this is the most beautiful piece of work I have seen in some time. If more people were willing to be a little crazy we might not be quite as tangled in spaghetti.

You realize there's such a thing as over-specifying something, right? You realize that using source code as a spec does this?

If you don't realize; consider that non-data aspects of a program, such as runtime and memory usage and bug compatibility, can sometimes form part of a specification, and sometimes don't. A specification says as much what is not required of an implementation as what is required. By claiming your one true implementation is the spec, one has no means of ascertaining what behavior is incidental, and what is actually required/able to be relied upon.

I'm not normally an XKCD fan, but this strip sums it up perfectly: http://xkcd.com/1172/

.

"""Hoon can be classified as a pure, strict higher-order static type-inferred functional language, with co/contra/bivariance and genericity. However, Hoon does not use lambda calculus,"""

A higher-order functional language does not "use" the mathematical definition of higher-order functions? In that case, what do you mean by "higher-order functional language"?

EDIT: I was going to make an analogy to the hypothetical claim that language X's arithmetic system doesn't use Church numerals (i.e. the mathematical formulation of natural numbers)… but Hoon is actually implemented using Church arithmetic. Go figure.

.

"""unification,"""

By what mechanism does Hoon implement type inference? Honestly, that's kind of like saying Hoon doesn't use, say, queues. Great, but, why?

.

"""or other constructs from “PL theory.”"""

Disdainful much? I'm really curious what's the background behind the scare quotes here.

.

EDIT: Just to be clear, I'm not claiming your project is uninteresting or not worth your while. I just feel you're being overly dismissive of the, let's say "traditional" schools of thought, with invalid justification.

There's a very important point in that Nock can specify not what a computer computes - but what it has computed, if it terminates. In general, practical systems have to interrupt long-running computations, so they must always compute some subset of that definition. But it can be, and is, a strict subset. I find this a meaningful and accurate statement.

Sorry, I didn't mean "PL theory" as scare quotes - I just didn't want to exclude anyone for whom the term doesn't instantly bring to mind a body of work.

The truth, though, is that the "PL theory" we have is just one theory of programming. It's a convention, it's not a piece of reality like pi. Church-Turing equivalence tells us that we have infinitely many such representations.

Eg, the Turing Machine is equivalent in power to lambda, but much less useful as a programming framework. My feeling is that, as a programming model, lambda suffers from the fact that it was originally designed, by mathematicians, to do mathematics.

Just from a UI basis, programmers are not mathematicians. The skill is very similar, but mathematicians work best in geometric and logical abstractions, whereas programmers are more comfortable with mechanical representations.

For instance, the general lambda approach is to represent data as code (Church numerals), a very sensible approach from the math side, whereas the Nock approach is to represent code as data - which feels more natural to the programmer.

So, nothing can tarnish the very powerful and elegant model of computing that is "PL theory." But it is not "the" theory of computing - just one of infinitely many possible theories.

I find Hindley-Milner inference systems too powerful. The programmer has to model what the inference system is doing in his or her head, and it's a source of significant cognitive load. Hoon's inference algorithm is slightly too smart in some cases, and requires slightly too much typing in others, but I think it's generally well matched to human capacities - especially for those of us who are not natural mathematicians.