Taking money out involves a contract on the main chain that, if the manager doesn't fulfill it cheaply and promptly, can be automatically fulfilled at the manager's expense. Disputes are resolved via interactive proofs paid by the loser — Game Semantics FTW!
-
-
Show this thread
-
Issue: anchoring the side-chain into the main-chain requires interactive proofs of mutual properties of both chains. Solution: each chain must thus offer a logically consistent model of its own evolving semantics as an API to the contract language.
Show this thread -
Since the least discrepancy between the many models in question or their many evaluators would be Ethereum-style million dollar disasters, it all better be specified in Coq with proven-equivalent extractors for the many languages involved.
Show this thread -
All in all, that's work for several researchers and PhD students for several years, much more than "just implementing yet another shitcoin". But the greatest use of Coq, ever, if it happens, with plenty of positive side-effects.
Show this thread -
Last point: each party of every interactive proof must grant its adversary enough time to answer its challenge that censorship on the main chain can reasonably be excluded. And to disincentivize a targeted DDoS, after a timeout anyone can take on the challenge.
Show this thread
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
Read my blog!