The entire and only possible point of a "smart contract" language is to bind two signed event structures ("blockchains") together. Thus these languages MUST be in terms of logical invariants of such structures, and to allow for universal quantification MUST be interactive proofs.
-
-
What more, unless you have
#Urbit-like confidence that you'll write the perfect system that (when complete) will never ever need to change, you MUST offer an API such that the interactive proofs that underlie contract enforcement still work when *either* protocol is upgraded.Show this thread -
Since the two protocols evolve separately, each blockchain MUST include a complete up-to-date reflective description of itself and its history, from which to extract logical fixpoint for the proof — with enough heads up to finish proofs that back out of problematic contracts.
Show this thread -
Since the least semantic discrepancy is a billion dollar disaster in the making, serious smart-contract blockchains MUST be written in Coq (or equivalent), with extraction to OCaml for the blockchain itself, and to interactive proofs based on a reflective model for the contracts.
Show this thread -
If the
@TezosFoundation ever gets out of its judicial rabbit hole, I'll make a case for it to fund a research program to this effect. If not, I'll go make a better coin, possibly by forking#Tezos.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!