Writing perfect, bug-free code is merely the first hurdle when designing a smart contract. You also need the code to cover all possible situations correctly. It

Writing perfect, bug-free code is merely the first hurdle when designing a smart contract. You also need the code to cover all possible situations correctly. It's here that smart contracts run into the mess we call the 'real world', and there's no proof of correctness that covers that. Smart contract creators need to be perfect programmers, but must also take their programming blinkers off and consider actual usage too. For example, a few weeks ago, there was a news story about an ethereum prenuptial agreement : http://www.coindesk.com/prenup-ethereum-marriage-obligations/ http://www.coindesk.com/prenup-ethereum-marriage-obligations... : https://drive.google.com/file/d/0B1MEGeLr7lWiNEE2U2lGdGFvSm8/view https://drive.google.com/file/d/0B1MEGeLr7lWiNEE2U2lGdGFvSm8... Ok, obviously a dumb idea, and not serious (I hope?) But take just one of the contract terms: 'It is stipulated that both the parties should spend at least 100 minutes every 10 days on a date-night' As someone in r/buttcoin wrote at the time: "In the last ten days, User 1 spent 5 nights at home, 1 night in a wrecked car and 4 nights in Lakeville Hospital. Date night clause has been broken. Marriage terminated." My point is that coding is the least of the problems with a smart contract. There needs to be a way to handle unexpected circumstances. In the real world, courts do that. In smart contracts, you're out of luck.