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!

Stepping away from the Algol keyword tradition is obviously a risk. At the same time, after using a keyword-free syntax for a while, reserved words feel really weird.

Someone just emailed and pointed out that he couldn't check out Urbit on Windows, because it has a file con.c. Oh, right, reserved filenames. How are reserved words different? The difference is - you're used to them.

Also, perceived usability (while it matters for marketing) is not the same thing as actual usability. Actual usability is something you only find out when you try to actually use something. We have a good bit of experience inflicting the syntax on coders of various abilities and backgrounds, and we're pretty satisfied with the result.

It helps that the syntax is quite a bit more regular than it appears at first glance. It's much more regular than Perl, and it also comes with a vocalization model that makes it easy to say out loud.

For instance, "=+", which more or less declares a variable, is "tislus." A lot of things like "=+" also start with "=", ie, "tis." You wind up learning about a hundred of these digraphs or "runes," which is a lot less than, say, Chinese.

Speaking of Perl, have you heard - Larry Wall is a Christian? I don't think this makes Perl a Christian programming language, though.One of the joys of our engineering inheritance from the 20th century, which was really humanity's golden age of political insanity, is that we get to stand on the shoulders of loons. We fly Christian astronauts into space on Nazi rockets programmed by Communist physicists. And it works...

You can represent them symbolically, of course, as you do for instance in XML.

Yes - although actually achieving this result in practice (and efficiently) takes a lot of doing right.

Excellent question!

One, as we know from Church-Turing equivalence, lambda and infinitely many other models of computing have the same expressive power. That doesn't mean they have the same practical utility, though.

Lambda in its Lisp incarnation is actually a rather poor substrate for something like a Lisp machine, I think, because it doesn't layer very well. You can define quite a simple Lisp model, but when you want to turn it into a practical Lisp, you don't add another layer - you grow hair on top of the existing layer. You grow a little hair, you get Scheme; you grow a lot of hair, you get Common Lisp.

I've never seen a lambda model (Qi/Shen perhaps a partial exception, but even there the underlying model is not very simple) that layers a complex language on a simple kernel. I think this is because lambda defines abstractions like symbol tables and function calls, which are user-level language features, in the computational model. The bells and whistles get mixed up with the nice clean math.

Another example is the fact that a modern OS should present itself to the programmer as a single-level store, meaning effectively an ACID programming language in which every event is a transaction. So, you're not constantly moving data across an impedance mismatch from transient to persistent storage, each having its own very different type system and data model.

But, if you're building persistently stored data structures designed to snapshot efficiently and remain maintainable, you really want your data model to be acyclic and not require GC. This goes in a very different direction from almost all the dynamic language work of the last 50 years.

Or, for instance, if your system is designed to work and play well in a network world, it really ought to be able to be good at sending typed data over the network. And validating it when it gets to the other side. Your type system ought to be able to do the same job as an XML DTD or JSON schema or whatever. Well... this wasn't exactly a design requirement when people designed, say, Haskell.

I could go on - there's a lot of stuff like this that is built the way it is because it made very good sense in the 60s, 70s, 80s or 90s. But the requirements really have changed, I think.

Or as I sometimes say: "on the bottom it's a new kind of math, on the top it's a new kind of social network." This is kind of shameless hype but not as much as you might think.

Sounds like a 10-year research project, right? Actually I started working on Urbit in 2002, as a sort of "unsupervised PhD thesis." I figured it'd be done by 2008 or so.

We seeded a startup last fall and are busy turning a prototype into a product. You can now write a pretty decent web app in Urbit, but it's still too raw to stand the light of day. For instance, the network works, but we often run global flag days when we shut the whole planet down and change the protocol.

One of the main problems with Urbit is that extraordinary claims demand extraordinary evidence. If you're going to ship something this crazy, it has to work extremely well right out of the box. We had a sort of abortive non-launch last year when the project kind of got accidentally leaked, and decided we had to "unlaunch" and go back into quiet mode. I hate selling things I can't quite deliver.

Edith Piaf said it best: https://www.youtube.com/watch?v=fFtGfyruroU

House is an OS in a very different sense than Urbit - the "boots on bare metal" sense. The core of House is a monad which represents the hardware state of a common Intel box.

Urbit is intended to run virtually in the cloud and is an OS only in the sense of "stores your data and runs arbitrary programs". As a cloud computer its "function" is simply (old state, packet in) -> (new state, packets out). For communicating with the host OS this generalizes to "event in" and "actions out." Eg, I got an HTTP connection so I send an HTTP response. So not only isn't it done, it isn't even very smart... but it is a function and it is an OS.

Thanks again for the advice.

Do you have a link to House? I wish people naming projects would realize that the Internet is dead and all we have is the Googlenet...

Sorry our site sucks. We released accidentally and are more or less in "semi-stealth mode." You probably shouldn't be interested yet. Unless you like playing with semi-broken stuff. When it's not broken we'll let you know.

Urbit is indeed a purely functional OS, not super dissimilar to the OP's project. And it works at least well enough to run a chat server on its own network (which generated all those logs with "leaves the building"). But we ship no code before its time and we probably shouldn't even have a site up.

You'll enjoy the video though - it has good music, at least.

"This trick is well known to old-style functional programmers, they waffle on about Y combinators and eat this stuff for breakfast, but it’s the kind of stuff that gives functional programming a bad name. Try explaining this to first year students who had a heavy night out at the pub the evening before."

Priceless (and completely true). I really think this attitude is why Erlang is such a success.

Oh, fine. Actually I mean codomain, because it's a conservative algorithm...

I agree with your goals but not with your observations. Perhaps I'm biased by the fact that I have small children. I am regularly amazed by their ability to memorize words, numbers, symbols, etc, combined with complete incompetence at abstract concepts. Grownups are different, of course, but it's still natural that most of what I know about learning comes from my own kids.

That's a truly amazing effort to take on the OS problem from a theorem-proving standpoint. I of course would try to attack the same problem on a theory-indifferent substrate. But... +1 for an exciting vision of math uber alles.

It is an understandable comment. Maybe we'll rethink it. Bad taste is a social construct, but you live in the society you live in...

On the other hand, the identity dialogue defaults unwary bros to %lady, which certainly ought to cause a little wailing and gnashing of teeth.

We have an asymmetry of discourse here, because you want me to take your disparaging remarks seriously. You also seem not at all concerned about your own appearance.

Yes, there is a purpose to the disparaging remarks. The purpose is to make this asymmetry apparent.

Academia in the late 20th century is something of a footnote to the great achievements of the 19th and early 20th. In this golden age of science, peer disparagement was more or less universal. It is only in the second half of the 20th, the golden age of grants as it were, that genuinely criticizing your peers becomes a faux pas, and team-building becomes the essential skill for a practicing scientist.

But wait, I'm not your peer at all. I guess I forgot that...

My definition of "rigorous and disciplined" comes from an entirely different world, the world of RFCs.

Here, you can look at my axioms and identify anything unrigorous or undisciplined about them:

https://github.com/urbit/urbit/blob/master/Spec/nock/5.txt

A bunch of people have written compatible implementations from the spec, which is the RFC world's general sanity test.

The ugly reality is that because of the actual mistakes the PL world (or even "academia" at large) makes, anything smelling of that world often is dismissed without a second glance. Even when it has genuine merit.

Tikhonj is right about this kind of "anti-intellectualism." But pro-intellectualism is a bias as well.

Basically, I'd say, ordinary human beings are much better at memorizing words and symbols than most smart people think - and much worse at understanding highly abstract concepts.

Think of the number of things you need to memorize to be an auto mechanic. Yet there are a large, large number of people who are capable of becoming auto mechanics, but not capable of becoming Haskell programmers.

An automatic castrator is an excellent safety device for your steer pen.

Generally we don't actually use these functions unless we're normalizing foreign data. Then, we do. Because anyone on the Internets can send a bull into your steer pen...

It does. And the best I can say is that I'm genuinely interested in the results of my experiment.

It would certainly be an interesting practical experiment to try to adapt a conventional syntax to the same semantics, or even to discard Hoon and create a more conventional language targeting Nock (which Urbit would have no trouble running).

I don't think so, but I wouldn't know enough to tell you. I can tell you that I am not very interested in 20th-century formal logic, at least as a way of defining programming, but you knew that. I think it seems like a logical equivalent that my approach is not very interesting from the standpoint of 20th-century formal logic.

Some UI burdens seem high, some are high. An interesting class of UI problem is the set of things that intuitively look difficult, but actually aren't.

Human brains are incredibly good at raw memorization of associations. Hoon has about 100 digraphs, and their internal structure isn't random. How hard is to learn 100 characters of Chinese? Perhaps easier than you think.

Nor are there no payoffs. For instance, most languages are very bad at defining large, mostly static hierarchical trees, so when it comes time to write code that generates, say, an HTML page, you reach for a special "template language" DSL. That's not a problem we have in Hoon. Also, most functional languages have a very annoying tendency to crawl off the right side of your screen and disappear, because indentation depth matches functional depth. That's also not a problem we have in Hoon.

So... you pay, definitely. But you also receive.

There's %wet but no ++wet. The name of the character is actually just the name of a parser function for it.

Am I not entitled to an opinion? You certainly are. You could tell me _why_ you disagree. And I would listen.

We may mean different things by "practitioners." I mean programmers. Unfortunately, your vocabulary is not common to programmers and shows no signs of becoming so.

Mine isn't either. But at least I've only been trying for a week. I know it seems strange to introduce new designs in the 21st century - most people assume, rightly of course, that everything worthwhile got figured out in the 20th.

Right, there you are with the definite article again.

What you're asserting is that without this system of rigor and discipline, there can be no other rigorous and disciplined way of defining programming languages. For one thing, this flies in the face of everything we know about the philosophy of mathematics.

I think my way of defining programming languages is pretty rigorous and disciplined. I'll continue to think that until you or anyone can identify some sloppy ambiguities. I note also that my foundation fits on a T-shirt and yours needs a math textbook...

s/the foundation upon which everything else is built/a foundation on which everything else can be built. If you'll accept this change, we don't disagree at all.

(Also, it is a serious overstatement to attribute Java and C# to PL theorists. Gilad Bracha is not James Gosling. PL theorists have contributed to some extensions to these languages. Typically, the extensions that confuse people and make them feel stupid.)

The difference between the foundation and a foundation is enormous, because (with your very large expensive foundation) you are asking programmers either to program without knowing the foundations of their work, or to learn a large and challenging body of mathematics.

And you know, higher-order typed programming is good enough that it's almost worth it. For most potential customers, however, learning PL theory does not seem to be worth it. Nor are they comfortable in programming in Haskell, a very powerful and complex environment, without understanding it.

It's this "the customer is just wrong" attitude that makes some of us sense an area ripe for disruption. Pride goeth before a fall.

Obviously if you have a door that needs to stay open, a thudingly concrete... never mind.

All I would say is, s/types/PL theory. Let's take your statement as true and stipulate that TAPL is in the top 1% of down-to-earthness of books on PL theory. Is it in the top 1% of down-to-earthness books on, say, Java? If not, what does this tell us about PL theory? You have read TAPL, right?

PL theory is a beautiful system and I've never said otherwise. TAPL is also very good at keeping doors open. But so are many things. PL theory is not the theory of programming, any more than TAPL is the doorstop. It is a theory of programming and a doorstop.

This sentiment takes many forms indeed. Think about your stereotypes of a vanished upper class, any upper class - for instance, the pre-revolutionary French nobility.

Obviously you never met any of these people, but you will find many negative stereotypes coming to mind. Are many of them true? Perhaps they are. Was the old Versailles full of charming, brilliant, talented, wonderful people? It most certainly was.

You might also have some stereotypes of PHP programmers. Perhaps they're true as well. No set of human beings is without patterns of fault. However, the PHP programmer is a peasant and cheerfully accepts the daily rain of mockery that falls on his head. He knows he is not above being laughed at, indeed he knows he is laughable, as all human beings are in some way laughable.

The distinctive feature of a privileged class, always and everywhere, is that it can't accept being mocked. Unfortunately this always increases the temptation to mock it, which I agree is a low and unproductive pastime. But anything to make type inference seem fun...

For the record, not that it matters, Sergey Brin was born in 1973 and started a CS PhD at Stanford, specializing in OS, in 1993. I was born in 1973 and started a CS PhD at Berkeley, specializing in OS, in 1992. Alas, neither of us finished.

Intellectuals are no different from anyone else - they live in the same reality and must be judged by their results. I don't think anyone would disagree that PL theory, as a body of work, has produced a set of languages whose penetration in the real world is oddly small both given (a) the investment in these technologies, and (b) the many real advantages of typed higher-order programming.

As a general pattern, usually when I see this outcome explained, it takes the form of blaming the user. We wouldn't let anyone else get away with this excuse, so why should intellectuals be treated as a privileged class?

To be anti-intellectual is to judge intellectuals more harshly than they deserve. To be pro-intellectual, also a cognitive bias, is to judge them more leniently than they deserve. In a world whose bias is generally pro-intellectual, it's easy for a neutral assessment to seem relatively anti-intellectual, but perhaps what you are perceiving is not an exceptional bias but the absence of a systemic bias which you've grown used to.