People who use low-level programming languages, or even functional programming languages, for their contract language, are completely missing the point.
-
-
Show 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.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 -
-
-
Do such languages need to be Turing complete or would a datalog-like language suffice? What about a TLA+ derived language? Clearly the implementation would need to be proved out. Turing completeness seems like overkill and a large attack surface.
-
So the meta-language is not just "Turing complete" but "logic complete", and yet the fragment (threatened to be) executed on the blockchain is designed to provably terminate, and in a known number of steps.
- 1 more reply
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!