Urbit: A clean-slate functional OS

http://www.urbit.org/

by tsax • 13 years ago

262 178 13 years ago

urbit.org

nutate3• 13 years ago

I really like this. I hope some younger people with more time on their hands push this farther.

tomrod3• 13 years ago

I'm not sure I follow what this is. Where would I use Nock and Hoon?

nutate3• 13 years ago

To build your startup? No.

To have fun? Why not.

theonewolf2• 13 years ago

I'm pretty sure this is a giant joke ? Or nothing is implemented yet (and still, kind of jokish especially in description)?

yebyen5• 13 years ago

Is this comment a joke?

I haven't tried compiling it, but even if large parts of the documentation say "this isn't finished yet" there are code and compilation instructions for Linux and OSX. If it's a joke then it's a joke that two contributors seem to have taken very seriously for a number of months now.

EDIT: Not like, say, Flynn... jab jab

theonewolf2• 13 years ago

I meant in a similar vein to say, esoteric languages or subsests like jsfuck.com.

I see this is considered more art, and I would agree with that.

It appears as if it is a large art + learning experience, and I appreciated that after I watched the movie.

Not a lot of _novel_ ideas per se, but an interesting mixture of things.

urbit33• 13 years ago

A demo video: http://vimeo.com/75312418

agumonkey• 13 years ago

This felt like an epilog to 2001 a space odyssey. Alien world.

mietek11• 13 years ago

The video shows an utterly fascinating mixture of Lisp, Erlang, Plan 9, and Bitcoin. The only missing ingredient is a proper static type system!

jsd19822• 13 years ago

I was with you til you introduced the Hoon syntax. Why ruin a great concept with a shit language? WHAT IS WRONG WITH LANGUAGE DESIGNERS?! Just come up with a sane language with a sane syntax on a great platform. This is apparently asking a lot. It's not fucking rocket science.

urbit33• 13 years ago

I agree entirely! This is so much better than the typical "middlebrow dismissive" that I upvoted it...

And actually, if you don't like Hoon you can build your own language on this platform. So long as it compiles to Nock. You'll probably have to write your first compiler in Hoon, but we do have pretty decent combinator parsers. If you can swallow the syntax...

jsd19822• 13 years ago

I like that you upvote your critics. That amuses me greatly. I had not viewed the video before I made my first comment but after watching the video I'm impressed with your implementation and solid practical concepts, but I still abhor your Hoon syntax. I haven't looked into Nock yet but I have a feeling I might knock its syntax as well, pun intended.

urbit33• 13 years ago

A better link would be the front page: http://www.urbit.org/

I guess on the Internets, you never release anything - it's released for you. Please be warned, (a) the doc is incomplete, (b) if you create an Urbit ship you'll eventually have to destroy it, as we don't have continuity yet.

tsax3• 13 years ago

Lame qn but does the name Albert Jay Nock have anything to do with 'Nock'?

urbit33• 13 years ago

http://en.wikipedia.org/wiki/Albert_Jay_Nock http://en.wikipedia.org/wiki/Tea_at_the_Palaz_of_Hoon

Four-letter names that haven't been overexposed are hard to find. But four letters fits in a 32-bit direct atom, so the attraction is pretty irresistible.

Touche2• 13 years ago

Watching the video blew my brains out the back of my head. Figuratively of course. Thanks for not letting me get anything productive done for the rest of the day.

msutherl• 13 years ago

The music is great. I stopped watching and just listened while continuing to get work done.

state2• 13 years ago

So here I am, in a submarine, learning a foreign language. What an afternoon.

eli_gottlieb• 13 years ago

Hoon is a high-level language which defines itself in Nock. Its self-compiling kernel, 7000 lines of code, specifies Hoon unambiguously; there is no Hoon spec. 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, unification, or other constructs from “PL theory.” Hoon also excels at handling and validating untyped data, a common task on teh Internets. Its syntax is entirely novel and initially quite frightening.

Crank detected. Homing in for the kill.

urbit33• 13 years ago

Have fun!

I recommend you start with the Nock tutorial:

http://www.urbit.org/2013/08/22/Chapter-2-nock.html

The build instructions in this file are out of date, use the ones from the Arvo chapter. Also, probably the best short overview is the header comment in the Hoon compiler:

https://github.com/urbit/urbit/blob/master/urb/zod/arvo/hoon...

Also don't miss the video: https://vimeo.com/75312418

nutate3• 13 years ago

Oh wow.

After watching the video I'm legitimately interested in more than the language. You've got some cool ideas going on there. I'll be emailing for a 32-bit destroyer in a second.

ajanuary• 13 years ago

So rather than having a lengthy standard it has lots of small non-standardized and brittle performance optimizations?

I remain skeptical over whether this tradeoff is worth it.

urbit33• 13 years ago

It's fairly easy to make them non-brittle, because it's very easy to rig a testing framework to run both the hand-optimized "jet" and the pure code, and compare them.

Standardizing performance is a subtler and more interesting point. It's a fairly safe bet that anything in the kernel that needs to be is jet-propelled. Above that layer, who knows? Good old normative text may handle it.

But in general, the feeling should be like the difference between hardware GL and software GL. The developer doesn't see it and the user sees it only as fast versus slow.

jamii2• 13 years ago

What about when the pure code is too slow to run? Or when the pure code is wrong but the jet is right - so that the nook spec is now not sufficient to determine semantics.

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.

lucian1900• 13 years ago

That's not entirely different from what a simple JIT does (or the unoptimised stage of a JIT without an interpreter).

wgd3• 13 years ago

I think it's a fascinating tradeoff. A typical approach with JIT-compilation is to write relatively inefficient code and hope that the JIT compiler picks up on it and optimizes it for you. Their approach seems to instead be to say "if you generate particular sequences of instructions, we'll detect those and instead execute a more efficient version, every time".

IMO this is a really cool idea because the performance optimizations are quite a bit less brittle than the ones you get with a JIT-compiled virtual machine.

nwmcsween• 13 years ago

This is what about 90% of the libc libraries out there do as well. Also tracing jits also do the same thing they see a trace that has a known optimization and it is performed.

jahewson2• 13 years ago

"if you generate particular sequences of instructions, we'll detect those and instead execute a more efficient version, every time"

This is what JITs do. At least the good ones.

dragonwriter• 13 years ago

A typical approach with JIT-compilation is to write relatively inefficient code and hope that the JIT compiler picks up on it and optimizes it for you. Their approach seems to instead be to say "if you generate particular sequences of instructions, we'll detect those and instead execute a more efficient version, every time".

I don't see the "instead" there. Those seem to be two ways of saying the same thing.

agentultra2• 13 years ago

This is really, really neat.

I really like the concepts in Avro and Urbit. Particularly interesting for me is the checkpoint/replay, distributed version control, and neighbours.

This is a really cool experiment!

urbit33• 13 years ago

Thanks, but Avro is someone else's cool project!

(Arvo is named for http://en.wikipedia.org/wiki/Arvo_P%C3%A4rt.)

agentultra2• 13 years ago

I think I've lost all precious free time I have... this is great stuff. :)

tlb• 13 years ago

You say addition is O(n^2), but I think you can write an O(n) addition with only increment, recursion, and equality testing.

In Python syntax:

  def add(a, b):
    return add_r(a, b, 0)

  def add_r(a, b, c):
    if b == c: 
      return a
    else:
      return add_r(a, b, c+1) +1

jcburnham• 13 years ago

Yeah... just one of the many many things we haven't gotten around to fixing. Since it doesn't really matter for a jet-propelled function.

https://github.com/urbit/urbit/issues/11

urbit33• 13 years ago

Yeah, it's true, the one in our kernel is O(n^2) though. Why? Because we're lame. But it hardly matters, as you'll never get anywhere with either O(n) or O(n^2) addition...

betenoire• 13 years ago

It's python, so it can't handle it either way, but by moving the final "+1" into the function call, it becomes tail-recursive.

  return add_r(a+1, b, c+1)

fyolnish• 13 years ago

This is art.

"There is never a reason to program in Nock. Except to learn Nock." Classic

saidajigumi• 13 years ago

For a project ostensibly inspired by K&R C, the copy on this site is amazingly opaque and full of its own rhetoric. Recommendation: delete all the linguistic posturing and get down to the hard work of casting light on your ideas. Let that speak for itself.

By way of example, the K&R C book had a beautiful clarity and ability to fluidly move between the realms of reference, spec, and tutorial. If you're going to hold K&R C up as a model, you'd do well to mimic its documentation philosophy.

wmf• 13 years ago

It seems like Urbit is art for art's sake. The fact that it executes is a side benefit.

(Oops, fyolnish beat me to it.)

urbit33• 13 years ago

That's an excellent criticism. Of course the problem is exacerbated by the HN link pointing to the philosophy doc. The greatest philosophy is to have no philosophy at all, but perhaps we're not quite there yet.

Actually the K&R equivalent for Hoon doesn't exist yet, and when it does it will be the first thing to read. Since it doesn't, the Arvo tutorial is the first thing to read:

http://www.urbit.org/2013/08/22/Chapter-1-arvo.html

But this itself is incomplete. Watch the video first:

http://www.urbit.org

Then build Arvo and use the sekrit code it generates to, basically, subscribe to our newsletter.

It's just a bad idea to document anything before it works completely, because you end up with doc that validates this criticism. The right way to build a language is to build it, use it, get comfortable with it, actually master it and become an expert of sorts... then document it. Sadly, not too many of us can live up to this ideal.

bjz_• 13 years ago

I for one love the whimsy. We need more LearnYouaThings and Shoes and runtimes that spit out lovecraftian quotes...

stuaxo• 13 years ago

I really enjoyed reading this + a some of the pages.

Very mindbending, got up to watching the video.

Am thinking it looks like it could be quite fast, I guess it would make sense to implement something like ContextFree in it as a start.

jahewson2• 13 years ago

I couldn't agree more. I don't want to know about how awesome the author is or how he's cunningly outsmarted everybody else. I'd like to see his ideas put forward without trashing other people's and with some theoretical context rather than just denunciations of PL theory.

Too much hot air.

groovy2shoes2• 13 years ago

I thought the style was a refreshing departure from the usual tone of expository technical documents. I actually enjoyed reading it, even though I disagreed with many of the assertions that were made.

lewispollard• 13 years ago

Personally, I was reminded of the schizophrenic guy on HN who built his own OS.

sr-ix• 13 years ago

I dig the Borges references riddled about.

jpt4• 13 years ago

From pedestal to pinnacle, all things are quantum, not classical. The metaphor that better avoids scaling obsolescence for your project is perhaps Bohmian, rather than Maxwellian.

noonespecial• 13 years ago

With all that jargon I was expecting a set up for a punch line at the end. Don't nock it so hoon, it's not done jet. Ha!

urbit33• 13 years ago

Sigh, HN really is turning into - never mind. :-)

quanticle3• 13 years ago

I love the project concept. A toy functional OS would be an admirable counterpart to e.g. MINIX. That said, I have one minor quibble:

A programming language is called a language for a reason - it should activate the human linguistic lobes.

Another programmer said this, a long time ago, and that's how we ended up with Perl. Please don't seek to emulate Larry Wall. Perl is great for quick automation, but anything complicated built with Perl quickly converges to unintelligible line noise (barring the exercise of zen-like discipline). If you're making something for beginners, please, please, give them the tools to build abstractions in a consistent and understandable manner.

urbit33• 13 years ago

Well, of course, Larry Wall is a god.

But that said, the main difference between Hoon line noise and Perl line noise is that most of the ASCII we use has a very regular structure, with a (relatively) limited set of exceptions. So it looks about equally alien at first, but the Hoon ideogram (digraph) set should be easier to learn. Unfortunately at present the set of people who know it is very small - so the theory really hasn't been tested.

It is what it is. But at least there's no Unicode. (Not that you can't have Unicode in strings, of course.)

And anyone who doesn't like line noise has to stand up for reserved words. Some of us welcome that conversation...

aray• 13 years ago

The unicode-in-strings but not in variables/etc bothers me about Java (coming from Go, where unicode is allowed in variables). It seems inconsistent to have two separate character sets for different semantic subsections of what is a single text file.

What about unicode in comments? If I put a string in a comment can it go there?

quanticle3• 13 years ago

I can search Google for reserved words. But I can't search Google for $@_{}

nmcfarl• 13 years ago

Larry Wall is a great man. And Perl was mighty force. An empire was built, and it may have crumbled, but all empires crumble.

One day you will be repeating these words, to a youngster that says the heroes of your Ruby palace, (or your conquering Pythonistas) were weak men of little vision, and laughs at you for following them. And when that day comes, I ask only that you think of me, and Wall, as I now think of one who followed Backus, and the mighty FORTRAN army.

pekk• 13 years ago

Python is about as old as Perl

quanticle3• 13 years ago

It's not age. C is older than Perl by decades, but I think C is a lovely little language. Lisp is as old as FORTRAN (almost) and I think it's probably the most elegant language invented yet. No, my quibble with Perl is that in throwing around implicit state everywhere (in an effort to make programming languages more like human languages) Perl is just bad as a system for building complex systems. It's not unique in this regard - Perl shares its weakness with the shell scripts it was supposed to replace.

cldr2• 13 years ago

Hoon is a keyword-free language - any alphanumeric text in the program is part of the program. Where other languages have reserved words, Hoon has squiggles.

But... why?

urbit33• 13 years ago

You're saying, why are reserved words a bad idea? I think most defenders of the humble reserved word would consider it, at best, a hack. Maybe it's a necessary hack, maybe not.

With reserved words you are overloading two very different namespaces, the space of language primitives and the space of user functions/variables. Sure, you can get away with this. But do you want to? A language is a UI, and the potential for confusing the programmer is immense. If operators and functions are really different things - as they are in Hoon, anyway - it's very confusing to mush them together.

Touche2• 13 years ago

Lisp has no reserved words.

cldr2• 13 years ago

I'm not asking why reserved words are a bad idea, just opining that I think having 100 single- and double-character symbols might not be the best UI for a language. Why not have just names (neither reserved like keywords nor inscrutable like symbols?)

I don't know, I am similarly annoyed by mathematicians because they usually use single letters for variables. It's a little more excusable for them because math functions are usually very short and have few variables, but still I'd rather use words. But I digress.

FeepingCreature3• 13 years ago

The alternative, as I see it, is to let people add new keywords to the language from inside the language, so there's feature parity again.

tsax3• 13 years ago

Brainfuck

alfredjaynock• 13 years ago

So this is what moldbug does in his spare time.

yebyen5• 13 years ago

I distinctly get the impression that the authors of this project will already know what Lojban is. This language (especially when you get to the part about reserved words, actually made up with special characters as runes, and how to pronounce them) made me think of the structure of Lojban right away.

For anyone who hasn't heard of it, http://www.tlg.uci.edu/~opoudjis/lojbanbrochure/lessons/

Urbit of course having the advantage that it can be programmed in... the video is very cool!

urbit33• 13 years ago

mi prami la lojban .ui

nemo16182• 13 years ago

ge'edai

Ixiaus• 13 years ago

The first time I have ever seen someone mention Lojban in the wild!!! How exciting!!

yebyen5• 13 years ago

Next I'm going to bring up the name FactorCode because I like namedropping languages :)

sz4kerto• 13 years ago

Astonished.

Reminds me a bit of A+, however. :)

mhartl• 13 years ago

Congrats on the launch (even if teh Internets did it for you)!

samograd2• 13 years ago

    So if we had to read the above decrement...we’d say: 
    “luslus dec sigfas cen dec bartis a tis pat sigbar soq
    dec soq ketcab pat wutgal tis pel zero a per tislus b 
    tis pat barhep wutcol tis pel a lus pel b per per b buc 
    pel b lus pel b per per.”

Absolute brilliance.

FeepingCreature3• 13 years ago

Well, I've read most the docs, let's say _skimmed_ the code examples, and I think you're a very smart, competent engineer with a sense of what makes for good language syntax that is utterly, incomprehensibly alien to me. So I guess, martian-language mission accomplished?

dreen• 13 years ago

Love the fact you used music by the god of ambient, Bran Eno.

quarterto• 13 years ago

  Hoon also excels at handling and validating untyped data, a common task on teh Internets.

Not sure if satire?

zzzmarcus• 13 years ago

Just some background, this is by Mencius Moldbug, a.k.a. Curtis Yarvin, a.k.a. C. Guy Yarvin of Unqualified Reservations fame. It's been in the works for a long time and is certainly a serious project.

http://unqualified-reservations.blogspot.com/2010/01/urbit-f...

http://moronlab.blogspot.com/

clarkm2• 13 years ago

Someone earlier in this thread mentioned his apparent disdain for PL research. If you want some background on his experiences, as well as some great musings on the current state of CS grad programs, I recommend these two articles:

http://unqualified-reservations.blogspot.com/2007/07/my-navr...

http://unqualified-reservations.blogspot.com/2007/08/whats-w...

mietek11• 13 years ago

I will not comment on the judgement passed upon the education system. The second article exhibits eristic tricks, obfuscatory language, and a plain confusion of ideas, especially when speaking about proof-carrying code and type theory.

It's interesting to see the author wishing for a Python of functional programming, and yet Hoon's syntax appears deliberately obscure.

However, there is one paragraph with which I wholeheartedly agree:

I think the world could use a charity that funds creative programming. The software systems that people use today — don't even start me on "Web 2.0" — are awful and ancient, and hardly anyone has any reasonable plan to improve them. Free-software programmers are not at all bad at supporting themselves, but nothing like Xerox PARC exists today, and it should.

It should, and, hopefully, it will. Soon.

samth• 13 years ago

The fact that it's by a guy who's an unreconstructed racist and thinks the US is inevitably headed for anarcho-capitalist dystopia (except that he doesn't think it's dystopian) certainly reinforces my initial opinion that it's nuts.

dmytrish• 13 years ago

Codex Seraphinianus of programming?

I think it's a true piece of postmodern art.

colanderman7• 13 years ago

"""Its self-compiling kernel, 7000 lines of code, specifies Hoon unambiguously; there is no Hoon spec."""

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.

urbit33• 13 years ago

As for the logical definition of a "spec," you are welcome to find any inconsistencies or imprecisions in the Nock axioms. Actually someone reported a (cosmetic) bug in the Nock spec this morning, which is quite cool.

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.

colanderman7• 13 years ago

As for the logical definition of a "spec," you are welcome to find any inconsistencies or imprecisions in the Nock axioms.

Not my point. The "spec" can be perfect, but you're not saying what a Nock implementation needn't do. If I write NockJIT that optimizes increment-loops into O(1) addition, does that violate the spec? You might reply "no", but someone else who relied on such loops for hardware timing obviously would say "yes".

andolanra• 13 years ago

"PL theory", the field of study, contains many, many theories of programming. There is not a lambda calculus, there are several (e.g. the untyped lambda calculus, the simply typed lambda calculus, System F, Martin-Löf's dependent type theory, among others) although not all of them are Turing-equivalent (the lack of which can be a useful feature), as well as other systems which are not based on lambda (e.g. concatenative calculi, which correspond roughly to things like Forth.) In fact, from a quick perusal, it seems that Nock is a minor variation on a graph rewriting system with the graphs restricted to DAGs, so... a studied and established theory of computation.

Similarly, there are techniques for representing code as data that are quite widely known and understood in programming language theory, e.g. through Danvy's defunctionalization or the use of arrows to make explicit the structure of computation or stage-separation and things like Lisp macros. These also are not ignored in the field of PL theory.

Effectively, my criticism is that your practical understanding of "PL theory" amounts to a mostly-remembered reading of "Types and Programming Languages," and so you are accidentally reinventing things poorly and describing them in an ad-hoc way. Now, Nock and Hoon and the others are quite interesting and impressive, and I plan to keep following them in the future, but I still assert that, rather than standing on the shoulders of giants as you could be, you've dismissed them as windmills and are trying to climb your own way.

urbit33• 13 years ago

As for the type inference, you don't need unification to do type inference. Hoon infers only forward, not backward. Of course you could say it's a subset of unification, as it is.

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.

tikhonj3• 13 years ago

What? Why do you have to think about what the type inference is doing? I've never needed that with H-M in practice, and I've spent a fair amount of time with both Haskell and OCaml.

When I use a good inference system like that, I simply don't think about the typechecker most of the time. It just doesn't come up. The types simply work out, largely because the inference is sufficiently good.

The only times I've had to model the inference in my head is when it is insufficiently powerful, like with OCaml objects or certain typeclass patterns in Haskell. That is, it's only a problem when the inference breaks unexpectedly.

Type inference just works, until it doesn't. And that's the only place I've had difficulties: when it doesn't.

The solution to a problem like that is not to make it break more often! That just exacerbates things.

A less capable system (say Scala or, god forbid, Go) just makes life more difficult. Even if it's easier to run the algorithm in your head. Especially then, in fact: you shouldn't be thinking about it on the first place.

colanderman7• 13 years ago

Of course you could say it's a subset of unification, as it is.

It definitely is, and a limiting one at that. How does Hoon infer the type error in whatever is the Hoon equivalent of the, say, JavaScript expression (a == b && b == 5 && a == "foo"), where a and b are function parameters?

freyrs35• 13 years ago

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.

Huh? I don't know what your type-inferred language of choice is, but personally I never have to go down to the level of solving constraint sets and unifying types in my head when working any of the ML dialects. Even when writing my own inference algorithms, once I'm able to establish confluence and progress I rarely give the main inference constraint solver a second thought when writing code.

batemanesque• 13 years ago

using "teh Internets" on yr front page is a great way to put off anyone who doesn't subscribe to calcified "geek culture"

wgd3• 13 years ago

The more I think about it the more I really like the whole "Jets" concept (although I'm not sold on the name, I'd love to learn that it's a known concept in the PL field with a nicer name). I'd like to see how such an approach would work out for optimizing something more "fundamental" like the Binary Lambda Calculus.

jamii2• 13 years ago

Haskell has rewrite rules which is how eg stream fusion is implemented.

http://www.haskell.org/ghc/docs/7.0.1/html/users_guide/rewri...

state2• 13 years ago

If ever there was a right attitude about bringing a radical project in to the world: this is it.

I just spent 15 minutes just _reading_ the documentation. Because it's _interesting_. That never happens.

0xdeadbeefbabe• 13 years ago

Reminds me of the punchline, "consider a spherical cow"

To a Pascal purist, to anyone who thinks mathematically, this seemed hideous. C isn’t really a high-level language at all - it’s a glorified macro assembler. Mankind retreats to the cave.

Leaky abstractions are hideous too, don't you think?

melloclello• 13 years ago

Hey Moldy I just want to say 'ur-bit' is a pretty cool name B-)

eonil2• 13 years ago

Though I couldn't understand them fully...

The names are awesome! The concepts are awesome! And the music is awesome!!!

eonil2• 13 years ago

I see some similarity to Smalltalk or Windows PowerShell. And this made me to imagine typed Smalltalk/Objective-C style syntax on shell which would be great for usability...

offensivehandle4• 13 years ago

Shell programs are expected to take streams of data and produce other streams of data. Shell programs are also supposed to, but often don't, have uniform configuration options. Instead, we have ps ax | grep chromium | grep -v grep | awk '{print $1}' | xargs kill

* ps accepts ax with no -

* awk is its own programming language lol

* xargs gets pretty complicated if anything bigger than this happens

(incidently, I know about awk '/chromium/ {print $1}' and killall. but i have seen that command line in the wild. because some people don't read the awk manual for fun, and i'm not sure if every unix system even has a killall command)

...and yet the shell is still the preferred tool for what it does because everything else requires too much typing (of both varieties)

Apparently urbit also has streams of raw data. It's about time someone came up with a new idea for a shell that keeps what's great about the shell (though personally, i would standardize on streaming a form of json, because it turns out that data is very often found as scalars, lists, and mappings).

So anyway. If urbit actually ends up being better to live in than unix, and having shell programs that are configured in exactly one way would be an improvement, and having data that's easier to parse than plain text while remaining as easy to read as plain text would also be an improvement, well, I've always wanted to live in a submarine. If it gets a nice editor and c++ compiler, that is. I do need the best performance possible out of my computer for my work.

arh68• 13 years ago

Would you mind doing lots more screencasts? Maybe writing a jet, rigging a test, profiling, and maybe a bunch of other things. I very much like your demo style, and I have a hunch these docs are going to be pretty dense. ;)

jyf1987• 13 years ago

so its root in forth?

cdcarter• 13 years ago

I can't tell what I'm more confused/impressed by, Hoon or the social model. Either way, I've got a destroyer and now I'm trying to understand just how zod works.

perlgeek• 13 years ago

A VM that can be precisely described in 200 words? Does that include the IO subsystem? I have my doubts that it's possible to describe a full set of IO operations that any modern VM needs in so few words, just because of the wealth of features that you usually need (file system access, sockets (TCP and UDP), pipes, IPC, ...)

dancecodes3• 13 years ago

video not work in ff linux

offensivehandle4• 13 years ago

i just finished watching it in firefox on a freshly-installed linux mint 15

dancecodes3• 13 years ago

nothing appropriate, gentoo and Im too lazy for fixing it (=^‥^=)

dancecodes3• 13 years ago

without flash of course there

JulianMorrison• 13 years ago

I love this concept of jets and how it allows a "completely isolated" VM to magically grow connections to the real world.

gwern• 13 years ago

I ate something I shouldn't have the other day and ended up having this surreal dream where Mencius Moldbug had gotten tired of the state of the software industry and the Internet and had made his personal solution to it all into an actual piece of working software that was some sort of bizarre synthesis of a peer-to-peer identity and distributed computing platform, an operating system and a programming language. Unfortunately, you needed to figure out an insane system of phoneticized punctuation that got rewritten into a combinator grammar VM code if you wanted to program anything in it. I think there even was a public Github with reams of code in it, but when I tried to read it I realized that my computer was actually a cardboard box with an endless swarm of spiders crawling out of it while all my teeth were falling out, and then I woke up without ever finding out exactly how the thing was supposed to work.

http://lesswrong.com/r/discussion/lw/ipu/open_thread_septemb...

offensivehandle4• 13 years ago

Okay, since you want comments here, here I'll put mine.

The reason you were so successful in coming up with a new political philosophy is that your "I'm a Martian" trick got you think thoughts that no respectable person would be caught dead thinking.

There aren't the same taboos in computer system design, so while you can refer to the systems people use every day as gigabytes of, what was it, of ass fucking more ass, there's nothing you say that I haven't already heard.

I'm still waiting for the Python of functional programming. Paul Graham announced Arc when I was in middle school. Maybe it will be released as the scripting system in Half-Life 3.

Being an alien from Alpha Centauri, and observing the growing collection of programming languages, what do you think people keep designing new ones for? Why do some Urplatians argue for Scheme and other Urplatians for Python?

Rather than asking the question of 'what is a programming language', and trying to design the axiomatically simplest possible thing, try asking the question of 'how do people use programming languages'.

Is your system a bit of syntax regularization away from the pseudocode people scribble on paper to explain algorithms to each other? No, that's Python.

Is your system something that compiles down to use the bare metal to its fullest potential while maintaining as much creature comforts as possible? No, that's C++.

Is your system something with an ancient history of having a solid ABI, that in fact every other language's ABI is described with? No, that's C.

Is your system a heap of cruft upon kludges with the original intention of providing programming access to a hypertext document? That's Javascript.

I wouldn't want to write a regex as anything but a regex.

In conclusion, you're asking a question that's been asked before and getting an answer that's been gotten before. But, maybe it is finally time for functional programming to come back. Maybe you're a popular enough guy to get people to use your system.

davidgerard• 13 years ago

"Being an alien from Alpha Centauri, and observing the growing collection of programming languages, what do you think people keep designing new ones for? Why do some Urplatians argue for Scheme and other Urplatians for Python?"

Typical mind fallacy. http://lesswrong.com/lw/dr/generalizing_from_one_example/

Most people model other people as just like themselves, plus or minus a diff. The trouble is that they don't understand just how wide-ranging human thoughts and feelings can be, and assume they will understand and be able to model based on the diff, even if the diff is larger than their whole mind.

It's why geeks keep coming up with "intuitively obvious" schemes no-one else can understand, and why engineers are routinely surprised at what actual end users do with their products in user testing.

So people write new languages that suit their personal peculiar ways of thinking. Thankfully, many are quite aware that this is what they are doing and don't claim universality.

This is why Urbit is art: translating numbers and ASCII characters into nonsense syllables that you are actually expected to pronounce and think in suits Yarvin's mind, even as it leaves me thinking "there is such a thing as being too much of a Borges fan". Which is absolutely fine. But this is why Urbit is art (an expression of a unique personal vision), not anything people are actually going to use without similar levels of confusion to the present.

For an example of fully rampant Typical Mind Fallacy in Urbit, see the security document: http://www.urbit.org/2013/08/22/Chapter-6-security.html About two-thirds of the way down, you can actually see Yarvin transform into Moldbug and start pontificating on how humans communicating on a network should work, and never mind the observable evidence of how they actually have behaved whenever each of the conditions he describes have obtained. The very first thing people will do with the Urbit system is try to mess with its assumptions, in ways that its creators literally could not foresee (due to Typical Mind Fallacy), though they might have been reasonably expected to (given the real world as data).

Urbit: A clean-slate functional OS

Related Stories