typish

"ipfs dht findprovs <hash>" gives the hash of the nodes serving it. I'm not sure how to get from that to an IP.

They could take an approach similar to how Freenet does dynamic things. See here for details: http://draketo.de/light/english/freenet/communication-primit...

Freenet has a similar immutable datastore but chat, microblogging, etc have been built on it.

I'm not sure what you mean. When I said that this is what Inferno provides I was referring to the parent posts request for their ideal computing model, not comparing to the Microsoft demo.

Without a solution to everyone needing to pay for a certificate and identify themselves this seems a bit premature. Maybe browsers will relax the "This is an evil self signed certificate on the site" warning when they do it.

Also interesting is their F* language: http://fstar-lang.org/

"F* is a new higher order, effectful programming language (like ML) designed with program verification in mind. Its type system is based on a core that resembles System Fω (hence the name), but is extended with dependent types, refined monadic effects, refinement types, and higher kinds. Together, these features allow expressing precise and compact specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using an automated theorem prover (usually Z3) behind the scenes to discharge proof obligations. Programs written in F* can be translated to OCaml, F#, or JavaScript for execution. "

It's open source too: https://github.com/FStarLang/FStar

This is something Plan 9 or Inferno (http://inferno-os.org/) would give you. You can run the main OS someone and mount the resources on other devices - including display, net and CPU resources. An example of doing this with a phone is here: http://bluishcoder.co.nz/2012/11/07/sharing-computer-and-pho...

Inferno is a portable and can be run on host operating systems. It would be possible to build it as an app on Windows Phone, Android, etc to access your Inferno resources on other devices.

That's not what Arstechnica is saying (regarding the recompile - they just need to publish to the store):

"Unlike Islandwood, which will require developers themselves to recompile their software to bring it to Windows, Astoria will in principle work with any old APK, without requiring the developer to do anything but publish the app in the store—as long as the APK sticks to the APIs that Astoria will provide."

It's a similar isolating feeling on Pitcairn. There's no air access so I arrived via a two day boat trip from Mangareva. Once there my boat left leaving me with no way off for the time I was there until another arrived to pick me up. You become very aware of how problematic a medical emergency would be.

For an example of such, here's one travellers tale of their medical evac from Pitcairn: http://jimmyaroundtheworld.blogspot.com/2010/09/life-and-dea...

When the outside world came into contact with the Pitcairn settlement there was one mutineer left, John Adams. There were Tahitian women alive as well who were part of the Bounty story, having been retrieved from Tahiti after the mutiny.

One of them, Teehuteatuaenoa, gave her account of the aftermath in an interview from Tahiti: http://www.fatefulvoyage.com/pitcairn/pitcairnDJenny.html

More on Teehuteatuaenoa and the history here: http://www.demtullpitcairn.com/teehuteatuaenoa.html

The island did suffer from lack of resources as the population grew. This lead to two migrations. One to Tahiti in 1831 and another to Norfolk Island in 1856. The latter is where many Norfolk Islanders can claim their ancestry from. Some islanders returned from Norfolk and re-settled Pitcairn soon after that migration.

With regards to genetic diversity, there have been many 'outsiders' that have settled and married with islanders. These were often the result of visiting whalers and shipwrecked sailors. You'll find most of the ancestral lines on Pitcairn have a mix of the initial mutineers, their Tahitian wives and outsiders giving genetic diversity.

Liquid Haskell might be what you are looking for: http://goto.ucsd.edu/~rjhala/papers/real_world_liquid.pdf

An example from that paper:

    type Nat = {v:Int | 0 <=v }
    type Pos = {v:Int | 0 < v }
    div :: Nat -> d:Pos -> {v:Nat | v <= n}

The ATS programming language (http://www.ats-lang.org) is more ML-like than Haskell-like but can have ranged integer types. Something like:

    fun slice {n:int | n >= 1} (a:int n, b:list)

I visited Pitcairn Island a few years ago, staying with an island couple. It's a great place to explore and I found the islanders friendly and welcoming.

There is an aspect of wariness I think with outsiders amongst them - especially those who are journalists or involved in media in some aspect. They've been bitten before and had their lives written about (Dea Birkett's book Serpent in Paradise comes to mind).