Hacker News new | comments | show | ask | jobs | submit login

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 circumstances - and it sure wasn't possible when making Hoon first compile itself. So, as inevitably in the real world, there is no substitute for not screwing up.

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.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact