You are viewing a single comment's thread from:
RE: Formal Verification of Smart Contracts and Wren
Possibly a stupid question but . . . . doesn't Rice's Theorem preclude Turing-complete language programs from being formally verified?
Possibly a stupid question but . . . . doesn't Rice's Theorem preclude Turing-complete language programs from being formally verified?
That is a very good question and it would take an entire blog post to answer it fully. Short answer is you don't formally verify the programming language, but you do verify the programs (Programs = Proofs). There are different methods of doing that and in the Ethereum example in the paper Solidity is translated into F* which is a functional programming language that makes formal verification a straight forward process. Programs can be formally verified by many different methods and my understanding of Rice Theorem is that certain problems are undecidable, but you can always determine when the finite program terminates, you can avoid infinite loops. With MSOL over graphs which appears to be state of the art, you can express any finite computer program. You have the benefit of a consistent logic MSOL and my understanding is that any software written under this logic ultimately is correct at the compiler level because formal verification could constrain unexpected behavior. But I will also say, because the ideas and papers are so new to me, I may not fully understand it, and Ohad himself may not fully understand it, because this is on the bleeding edge of what is possible. What we can do is simply research it together and blog about it but my current understanding is you can do formal verification but some problems remain undecidable due to Rice's Theorem.
References
https://www.cs.ox.ac.uk/people/luke.ong/personal/publications/lics06.pdf
I would love to research it and blog about it together. I am very interested in getting into smart contracts and really do think that it would be an awesome doable project for the hackathon . . . . https://steemit.com/steemit/@mark-waser/less-than-hack-ether-camp-greater-than-a-4-week-virtual-hackathon-to-build-out-steem-tools-1st-prize-usd50-000.
I've been doing a lot of thinking about how much is required in terms of necessary hooks available from/provided by steem and how society-based escrow/bonding is most effectively performed.
Once there is a smart contract capability for Steem via sidechain then I think we will see a flood of smart contracts. Let's hope we get this smart contract functionality in an upcoming hard fork.
Clearly there is a lot of demand from developers for this functionality because you see so many apps so soon.
#hassan #rouhan #steven #spielberg
https://steemit.com/news/@cryptocurrency1/https-www-youtube-com-watch-v-iovkjhu7mfk
Your question reveals how difficult it is to write correct programs and I found this video:
The video seems to illustrates what your question leads to. So we can never fully know certain things and the video mentions reachability and Rice's Theorem.
Reference