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.
-
-
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 -
-
-
As long as protocol upgrades have enough of a heads up, short-term contracts may only have to deal with simple predictable protocol changes, if at all. On the other hand, permanent or long-term contracts need a way to deal gracefully with those inevitable changes.
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
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!