Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Urbit: A clean-slate functional OS

urbit.org

Post reply on HN
Print view View original

151–160 of 185 posts

Re: Urbit: A clean-slate functional OS

#151

Post by sstewartgallus »

urbit wrote: post #103
jamii wrote: post #82

Earlier quoted context omitted.

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.

Thanks, and you're right about both problems. One, it takes a good bit of work to boot Arvo beyond a merely correct nock interpreter. The Hoon type system, for instance, is enormously painful if not jet-propelled. Two, the kind of bug you're describing is in fact the nastiest class of bug. The best way to get around it is to always make sure you write the pure code first. But this isn't possible in a variety of circu…

Because Nock is so simple (just a few substitution rules) I wonder if it'd be reasonable to formalize it in a theorem prover like Coq, or Agda to ensure correctness.

Re: Urbit: A clean-slate functional OS

#152

Post by freyrs3 »

andolanra wrote: post #149
urbit wrote: post #86

Earlier quoted context omitted.

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 computatio…

"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. concatenat…

Arguably there's a lot of folks reinventing things poorly in ad-hoc ways, doubtful that will ever change. What's more concerning is the flagrant anti-theory attitude that, at least to me, seems to be on the rise. In the context of discussions around Haskell or Agda it's sadly common to see "mathematical" bandied around as a synonym for "impractical".

Re: Urbit: A clean-slate functional OS

#153

Post by nightski »

richardlblair wrote: post #59
tomrod wrote: post #29

Earlier quoted context omitted.

I should rephrase my question: on what technology platforms would one use Nock and Hoon? Embedded systems? Anything (due to "portability")?

As others have pointed out, this is art. You don't look at art, and ask "Why did you do this??". You simply enjoy it. The artist did it, to do it, and nothing further. If you can not see this that way, then I am truly sorry.

If it is truly art then it doesn't make much sense why he is trying so damn hard to make it practical.

Re: Urbit: A clean-slate functional OS

#154

Post by perlgeek »

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, ...)

Re: Urbit: A clean-slate functional OS

#155

Post by qznc »

mietek wrote: post #134
urbit wrote: post #67

Earlier quoted context omitted.

Yes. And that's what many people find so elegant about Lisp. But, one could argue, the "is it a function? or is it a macro?" confusion is a significant cognitive load on the Lisp programmer. These are really two different things, even though you can fit them into the same namespace. Hoon has the different problem that you allude to - it is hard to extend the macro set at the user level. While this is fairly limiting,…

In my view, CPU speed advances and a high-quality optimizing compiler mean there aren't many reasons to use macros in Haskell. People do, though; for examples of extensive Template Haskell use, see Yesod.

We are pretty much done with CPU speed advances and compiler optimizations. If you use an Intel i7 with the Intel C compiler, there might be a few percent left to optimize, but not much. Free lunch is over for a decade now.

You might get more cores at the same speed, but even that seems to be limited due to heat issues.

You can get more efficient CPU (e.g. SIMD instructions) but the compiler cannot optimize for them very well. Some people say implicit SIMD is a bad idea anyways.

Re: Urbit: A clean-slate functional OS

#158

Post by drewhk »

mietek wrote: post #130
clarkm wrote: post #112

Earlier quoted context omitted.

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...

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 whol…

Deliberately obscure, yes:

>We should note that in Nock and Hoon, 0 (pronounced “yes”) is true, and 1 (“no”) is false. Why? It’s fresh, it’s different, it’s new. And it’s annoying. And it keeps you on your toes. And it’s also just intuitively right.

Re: Urbit: A clean-slate functional OS

#159

Post by tomrod »

richardlblair wrote: post #59
tomrod wrote: post #29

Earlier quoted context omitted.

I should rephrase my question: on what technology platforms would one use Nock and Hoon? Embedded systems? Anything (due to "portability")?

As others have pointed out, this is art. You don't look at art, and ask "Why did you do this??". You simply enjoy it. The artist did it, to do it, and nothing further. If you can not see this that way, then I am truly sorry.

I see beauty in many things. I'm not yet at the level of programming where I see beauty in syntax -- maybe one day though!

Re: Urbit: A clean-slate functional OS

#160

Post by Peaker »

urbit wrote: post #76
Peaker wrote: post #74

Earlier quoted context omitted.

The Lambda Calculus is so tiny how can you view it as anything but trivial? Just 3 syntactic forms building up an expression tree: Expr = Lam Name Expr | Var Name | Apply Expr Expr And one reduction rule: reduce (Apply (Lam name body) arg) = subst name arg body At least assuming unique names (no shadowing nonsense), you can't get much simpler than this...

You can get rid of the whole name reduction system. Which is hardly trivial. If you assume it, though, it's true that everything else is trivial. Getting symbol tables, functions, environments, free and bound variables, etc, etc, out of the fundamental automaton, frees you up to design them right at the higher layer where they (IMHO) belong. This philosophical argument has serious practical ramifications, I think, be…

Lisp isn't really the only attempt to work with the lambda calculus.

Look at Haskell, Agda, and others, which are based on an a slightly extended form of LC. I doubt anyone would claim that these extensions are "hairy".

Post reply on HN