Ok, I just clicked on the link and what I saw there just didn't make any sense to me :-) Still doesn't now, but after reading the comments, I returned to the site and studied it more carefully. Maybe the link should point to chapter 0, not chapter 5, to have any idea about what this is about ... After reading chapter 0 now, I can understand the goal of urbit, and I think it is a great one! But note that you can work on exactly the same goal without leaving PL theory and theorem proving entirely behind you. Check out http://proofpeer.net to see how this might be possible.