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.
-
Show this thread
-
People who use low-level programming languages, or even functional programming languages, for their contract language, are completely missing the point.
1 reply 0 retweets 1 likeShow this thread -
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.1 reply 0 retweets 1 likeShow 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.
2 replies 0 retweets 1 likeShow 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.
1 reply 0 retweets 3 likesShow 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.
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!