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

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