Theory-wise, a Turing-complete system can emulate any other turing
   complete system unless the emulatee has an ace up its sleeve; something
   unique to the hardware that canot be simulated without breaking
   authenticity.
   This is probably only *theoretically* possible with quantum
   computation, but it's *practically* possible with tamperproof hardware:
   TCMs used for good instead of evil, maybe?

   On 28 July 2014 18:04:05 GMT+01:00, "Lodewijk andré de la porte"
   <l@odewijk.nl> wrote:

   2014-07-28 18:35 GMT+02:00 Georgi Guninski <[1]guninski@guninski.com>:

   > I have a rough outline for a "cloud computing grid" that verifiably:

     verifiably? _really_ provable stuff is a very scarce resource IMHO
     (especially in crypto. do you need crypto? Do you need P \ne NP?).

   Yes, it needs crypto. I said verifably because "proving" an
   untamperable hardware box (IOW: you can only plug it in, nothing else)
   is what the spec says it is, is, well, impossible.
   You'll depend on some observers, audits and where possibly physical
   impossibilities, to show that indeed it is what it is. It's not proof,
   but with trust you can verify it.
   It's as good as it gets, but no better. I don't think that'd surprise
   anyone.
   Part of the design involves generations. Eventually you'll have a
   generation for which something is questionable in a certain way,
   nothing to do about it. Generations will slowly die as the hardware
   breaks and the network becomes too small (has too few resources) to
   uphold anonymity and fault-tolerance guarantees.
   Perhaps a generation will be hybrid with blackbloxes mailed to people
   and satellites in space. That generation would be expected to
   deteriorate fast in the first 100 years, and then hardly deteriorate at
   all for many after that.
   All these different grids will have some sort of resource pricing
   scheme, that may guarantee a certain runtime, or may be subject to
   monthly renewals at new market prices or whatnot. It's a very
   interesting part of the design.
   But yes, the anonymity profits /greatly/ from crypto. Interestingly I
   think it could well work without crypto, whereas hardly any other
   designs could. It'd lose a lot of convenience though! And P = NP
   doesn't mean crypto is useless, just less nice. At the very least
   there'll be OTPs! Then there may be (quantum) couple RNGs that can
   generate secure OTPs. I think there'll always be ways the newer
   generations of this idea can continue to function.

     > But it absolutely requires a verified microkernel. I'm *very
     *excited to

   > see that we're making progress towards it.

     Is it really a progress?
     There are assumption free proofs of False
     in most formal proof systems.
     Design flaws like \lor instead of \land
     pass the verification process and later are
     considered design flaws, not bugs in proof IMHO.
     Knuth quote:
     "Beware of bugs in the above code; I have only proved
     it correct, not tried it."

   It's progress, because now all we need is to specify safely, or find a
   way to prove specifications. The rest is somewhat, maybe,
   experimentally operational. It'll depend on how well we use it, but it
   is a step in the right direction!

   --
   Sent from my Android device with K-9 Mail. Please excuse my brevity.

References

   1. mailto:guninski@guninski.com