[Zillion]

The choice of 0 for true and 1 for false is _wrong:_ On the Curry-Howard correspondence (and above) a type corresponds to a false sentence when it is not inhabited, like 0, and to a true sentence when it is. The Curry-Howard correspondence is fundamental, and so that is the. correct way to go, absent evidence in the other direction. I don't know whether Nock is a better foundation for a programming language than the Lambda Calculus, but it is at least as elegant—I'm glad someone is seeing where it leads I'm a fan of internet freedom, which often requires anonymity, and so I have my doubts about an OS that preserves exerything as a feature of the design.

[urbit]

IANAM, but I thought really if there was one great lesson of 20th-century mathematics, it's that nothing (ie, no system of axioms) is fundamental and superior to all others. For instance, Church-Turing equivalence does not tell you that Church's model of computing is more fundamental than Turing's or vice versa.

If you look at where lambda comes from, it comes out of this same project of metamathematics that originates in the 19th century with people like Frege - how do you describe math in terms of math? Then it was discovered that this project could be repurposed as a definition of computing. Reusing old standards is a thing that happens, but sometimes you'd come up with a different approach if you were starting from scratch. As I've pointed out elsewhere on this thread, the shared theoretical foundation of lambda does not lead to a family of languages that are compatible in any meaningful sense.

It was probably a bad decision to make 0 true and 1 false, but not for mathematical reasons. There is always a lot of C coupled to Urbit, and what ends up happening is that the easiest way to handle this problem is to write C in a sort of dialect in which 0 is true and 1 is false. This is slightly cumbersome, and the perceived elegance of 0 == true isn't at all worth it. However, it's also nowhere near awful enough to revisit the question, which would be quite tricky considering the self-compiling nature of the system!

[loqi]

It's been sorta mentioned elsewhere on the thread, but there is another (IMO simpler) mathematical intuition behind 0:1 :: false:true that doesn't involve any lambda fundamentalism. It's the algebraic analogy disjunction:conjunction :: addition:multiplication :: union:intersection :: ... which also turns up pretty often in computing.

For instance, if you've got anything like regular expressions, then you've got something with a structure where the "unit" (trivial match) is an identity for sequencing, and the "zero" (failed match) is an identity for disjunction and a zero for sequencing. It's not exactly a formal argument for preferring booleans to loobeans, but a failed regex match sure feels like a "false" to me.

I don't doubt that it's not worth changing at this point, but don't throw the semiring baby out with the lambda bathwater.

[jdpage]

Aside from the zero/one thing, if I'm understanding this right, Nock is based on the SKI combinator calculus, where the combinators are

S: λxyz.xz(yz)

K: λxy.x

I: λx.x

From there, you can express anything from the lambda calculus, and vice-versa. So I think it's reasonable to say that Nock is just a machine-friendly way of expressing the lambda calculus.

[urbit]

I wouldn't say it's based on SKI - just relatively similar. There are a lot of ways to skin this cat.

SKI is obviously a lot simpler mathematically, but I wouldn't want to try to use it as a compiler target...

[jacquesm]

The 'I' is optional, all you need is S and K. I = (SKK)

You can go simpler still: Iota.

[javaexpert101]

Or you could consider that they are freaking isomorphic to each other and therefore neither is better than each other